On Thursday, 7 August 2014 at 14:09:26 UTC, David Bregman wrote:
If you use the definition of assume that I gave, assume(P && false) declares the axiom

P => (P && false)

which is again equivalent to !P.

Well, P=>(P&&X) is equivalent to P=>X.

But you are allowed to have "false" in the preconditions, since we only are interested in

preconditions => postconditions

assume(input!=0) is ok… it does not say unreachable.
It says, postconditions are not required to hold for input==0…

Reply via email to