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.
