assert semantic change proposal

[Matthias Bentrup via Digitalmars-d]

On Thursday, 7 August 2014 at 06:32:18 UTC, Ola Fosheim Grøstad 
wrote:
> 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 :-).

So the D function (note that "a" is constant)

int silly() {
   enum int a = 1;
   if( a == 2 ) {
     assert( a == 2 );
   }
   return a;
}

has undefined semantics (at least in debug mode), because it 
contains a false assertion ?

That is not my understanding of assert.