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 axiomP => (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…