Let the interpreter execute the following three Worthwhile programs, each time the assertion (wrapped in a quantified expression so that the prover is asked as the interpreter does not yet take assumptions in consideration when evaluating simple assertions) should succeed since when the _assumes are visited false is assumed.
_assume false
_assert ∀ Integer i : 1 = 0
and
if (true) {
Boolean c := false
_assume c
}
_assert ∀ Integer i : 1 = 0
and
Boolean c := false
_assume c
c := true
_assert ∀ Integer i : 1 = 0
However, in the last two examples this is not the actual behavior (the annotations fail), because one time c is no more present in the environment and the other time c is reassigned (to true) before the assumption is evaluated. Both times the assumed expression is changed after it was executed.
Let the interpreter execute the following three Worthwhile programs, each time the assertion (wrapped in a quantified expression so that the prover is asked as the interpreter does not yet take assumptions in consideration when evaluating simple assertions) should succeed since when the
_assumes are visitedfalseis assumed.and
and
However, in the last two examples this is not the actual behavior (the annotations fail), because one time
cis no more present in the environment and the other timecis reassigned (to true) before the assumption is evaluated. Both times the assumed expression is changed after it was executed.