assert semantic change proposal

[via Digitalmars-d]

On Thursday, 7 August 2014 at 05:41:22 UTC, Matthias Bentrup 
wrote:
> If assume is independent of control flow, then clearly this
> cannot be related to assert.

Well, both assume and assert are "independent" of control flow 
since you don't have execution or control flow in mathematics.

The dependency is tied to the "renaming of variables into 
constants" which allows Hoare-Logic to work on variables, not 
only constants. However, for proper constants, you don't need 
that limit for neither assert nor assume?

if(B){
    assume(B && PI==3.14)
} else {
    assume(!B && PI==3.14) // must hold here too since it is a 
constant
}

apply hoare logic rule for if:

if this holds:

{B ∧ P} S {Q}   ,   {¬B ∧ P } T {Q}

then this holds:

{P} if B then S else T endif {Q}

which gives:

assume(PI==3.14)
f(B){
    assume(PI==3.14)
} else {
    assume(PI==3.14)
}
assume(PI==3.14)


(Usually you only have assume at the top in the preconditions, 
since you otherwise don't get a proof :-).