On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
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".
(Your understanding is the conventional one.)
Yeah, the one with control flow is really the only useful way to
define it, at least for use in an imperative language. If you can
only write assumes which are globally valid, then you can't refer
to local variables in the expression. That makes it pretty
useless.
As for assume(0), in the control flow interpretation it makes
perfect sense: Assuming control flow reaches here, false = true.
So by contradiction, "control flow reaches here" is false, i.e.
that point is unreachable.
see again the __assume extension in the Microsoft c++ compiler:
http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx
