On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
Right. So if X is false, the axiom we declare is !P, not
"false" or "a fallacy".
But Pn is always true where you assume…?
False => X is true for any X, so the axiom we declare is just a
tautology.
I don't follow. If any assumption is false then anything goes…
So is the control flow definition / unreachability argument
clear now?
Nope.
> 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.
assume(true)
r = calc()
assert(specification_test(r)) //required to hold for any situation
assume(false)
r=calc()
//r can be anything
// input!=0
assume(input!=0) // true
r=calc(input)
assert(specification(input)==r) // required to hold for input!=0
//input=0
assume(input!=0) // false
r=calc(input)
assert(specification(input)==r) // may or may not hold
