assert semantic change proposal

[via Digitalmars-d]

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 or that it cannot be proved by the the 
assumptions, hence the assumptions need strengthening.

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

implication is not equivalence

> After assuming 'false' you can prove false.
> ⦃ false ⦄ still means 'unreachable' if it is 'assume'd.

False only means that the postcondition does not hold. If the 
precondition is false then the triplet is valid i.e. correct.

> (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.

>> 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. 
Deduction lacks a notion of time.

> ⦃ P ∧ Q ⦄  // ← precondition
> assert(Q); // ← statement
> ⦃ P ⦄      // ← postcondition

Makes no sense. Assert is not an imperative statement, it is an 
annotation. It is meta.