On Wednesday, 6 August 2014 at 18:51:05 UTC, Ola Fosheim Grøstad
wrote:
On Wednesday, 6 August 2014 at 17:59:06 UTC, Marc Schütz wrote:
The crux is the axiom that is being defined. When you write
`assume(condition)`, the axiom is not:
"`condition` is true."
but:
"When control flow reaches this point, then `condition` is
true."
It's not an unconditionally true condition :-P
Assume(X) does not provide a condition. It defines a
proposition/relation to be true.
If you define a relation between two constants then it has to
hold globally. Otherwise they are not constant…
Assume(P) defines that the proposition holds. If it does not
involve variables, then it will be free to move anywhere by the
rules of Hoare-logic (and propositional logic)? If
assume(PI==3.14…) can move everywhere, by the rules, then so
can assume(true==false).
Ah, I had a different understanding of assume, i.e. placing an
assume(A) at some point in code adds not the axiom A, but rather
the axiom "control flow reaches this spot => A".
So if there was a different operator, assume_here() or so, with
the semantics that I incorrectly assumed for assume(), could the
optimizer insert assume_here() for assert() ?
