assert semantic change proposal

Matthias Bentrup via Digitalmars-d digitalmars-d at puremagic.com
Thu Aug 7 01:52:42 PDT 2014


On Thursday, 7 August 2014 at 08:35:21 UTC, Ola Fosheim Grøstad 
wrote:
> On Thursday, 7 August 2014 at 08:12:23 UTC, Matthias Bentrup 
> wrote:
>> 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 ?
>
> It isn't reachable so it is not part of the program? If you 
> support generic programming you probably should limit proofs to 
> reachable portions of library code.
>
> However the specification or the implementation of it appears 
> to be flawed, so perhaps it should be considered incorrect if 
> this was in application code.
>
> You usually try to prove post conditions in terms of pre 
> conditions. The invariants, variants and asserts are just tools 
> to get there. So this is not a typical issue.

So reachability has an influence, but control flow hasn't ?


More information about the Digitalmars-d mailing list