assert semantic change proposal

[Timon Gehr via Digitalmars-d]

On 08/10/2014 04:40 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= 
<ola.fosheim.grostad+dlang at gmail.com>" wrote:
> On Saturday, 9 August 2014 at 20:22:36 UTC, Timon Gehr wrote:
>> Formally, that's what it assumes to be the case. If you can prove
>> 'false', this means that the code is unreachable.
>
> No, if you prove false that means either that it is nonterminating

I.e. everything afterwards is unreachable.

>>         ⦃ Q ∧ ¬Q ⦄
>>         ⦃ false ⦄     // this means 'unreachable'
>>         assert(false); // goes through
>
> implication is not equivalence

Do you agree we indeed have equivalence for those programs with an empty 
precondition?

> or that it cannot be proved by the the assumptions, hence the assumptions
> need strengthening.
> ...

'false' is the strongest statement. Why would you need to strengthen 
assumptions?

>> (Yes, of course it can also be read as 'inconsistent', if the code is
>> actually reachable, but proving code 'unreachable'
>
> No, you can have this:
>
> main(){
> Precondition(false)
> Stuff()
> Postcondition(anything)
> }
>
> This states that Stuff has not yet been verified for any input. It does
> not state that Stuff will never execute.
> ...

If the precondition is actually assumed to hold for all executions of 
the program, a precondition of 'false' means that the program never 
executes. Maybe you don't assume this, but internally to the logic, this 
is what happens: You verify the postcondition under the assumption of 
the precondition. I.e. in this case you verify the postcondition of the 
program under the assumption that it never executes.

Of course you may still execute such a program, but the ⦃ ⦄ assertions 
become irrelevant to this execution.

Note that an optimizer needs to be able to use deduced facts for program 
transformations, or it is useless. To an optimizer, a contradiction 
means 'unreachable'. There are no non-trivial preconditions (in your 
sense, i.e. the program still may have interesting behaviour if they are 
violated) on the program used to deduce those facts. Do you agree that 
_if_ 'assume' is to be seen as an optimizer hint, then 'assume(false)' 
means 'assume unreachable'?

>>> Your "definition" is lacking. It mixes up two entirely different
>>> perspectives,
>>> the deductive mode and the imperative mode of reasoning.
>>
>> I think you should elaborate on this a little if you want to make a
>> point. E.g. I don't think that such an opposition of 'reasoning modes'
>> even exists.
>
> Of course it does, that is why Hoare Logic and SSA exist.

They exist for the virtue of being convenient formalisms for some 
applications, but they can be embedded into e.g. set theory just fine.

> Deduction lacks a notion of time.
> ...

What is 'a notion of time' and how does HL provide it?

>> ⦃ P ∧ Q ⦄  // ← precondition
>> assert(Q); // ← statement
>> ⦃ P ⦄      // ← postcondition
>
> Makes no sense.

It is a definition. If you actually want to understand David's point you 
should digest it.

Does

⦃ false ⦄
abort;
⦃ P ⦄

make sense to you?

The assert(Q); statement is equivalent to

if(¬Q) abort;


> Assert is not an imperative statement,

Yes, it may be seen to be.

> it is an annotation. It is meta.
>

If it is part of the program it is not 'meta'.

Here, there is a distinction between:

assert(P) // statement

and

⦃ P ⦄    // "meta"

even though both are commonly called 'assertions'.

assert(P); is a statement and hence it needs to be given a semantics, 
e.g. an axiomatic semantics or by rewriting, as above.


(BTW: This is not about being right or wrong. It is about understanding 
each other's statements in the right context.)