On Thursday, 7 August 2014 at 15:35:30 UTC, Ola Fosheim Grøstad
wrote:
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.
Right. So if X is false, the axiom we declare is !P, not "false"
or "a fallacy".
But you are allowed to have "false" in the preconditions, since
we only are interested in
preconditions => postconditions
That's ok. There is no contradiction if P is false.
False => X is true for any X, so the axiom we declare is just a
tautology.
So is the control flow definition / unreachability argument clear
now?
> assume(input!=0) is ok… it does not say unreachable.
> It says, postconditions are not required to hold for input==0…
And… assume(false) is a precondition that says that you don't
have to care about the postconditions at all… Basically,
"assume anything"…
I don't get this part, maybe you can reword it if I haven't
already answered the question.
