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.
