On Thursday, 7 August 2014 at 18:20:20 UTC, David Bregman wrote:
On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad
wrote:
I just gave you a concrete example of where assume(false) might
be useful for optimizing a switch statement.
But to me it sounds dangerous if it actually is reachable or if
the compiler somehow think it is. So you should use halt() if it
should be unreachable, and use unreachable() if you know 100% it
holds. Encouraging assume(false) sounds like an aberration to me.
You need to provide proofs if you attempt using assume(X) and
assert(false).
This is valid, but it is derived, not postulated:
assume(P)
while(false){
assume(false) // anything goes is acceptable over S here
S… // since it never happens…
assert(P) // valid since the assumption is false
}
assert(P) // valid since the content is just a noop
When you postulate without proving you open a can of worms:
assume(P)
while(B){
assume(false) // woops! Should have been assume(B&&P)
S… // ohoh we just stated anything goes in
here…
assert(P) // invalid
}
assert(P) // invalid since the loop invariant doesn't hold.
How do you define P1 and P2 to be different?
I'm not sure how you'd define them to be the same. They're
different lines of code, for one thing.
I don't believe there "is" such a thing as lines of code. We are
doing math. Everything just "is". We don't have code, we have
mathematical dependencies/relations. P1 and P2 are propositions,
so what are the content of those? The ones you use for your P1=>X
and P2=>Y? You have to define newassume(P,X)===assume(P=>X). But
what is P?
Anyway, you don't need those… You can use a regular
assume(false), but not for indicating unreachable. You indicate
that the postcondition does not have to hold. Otherwise you will
run into trouble.
But if you think about while() as a short-hand that is expanded
into pure math, then it makes sense. If you have while(true){}
then the loop cannot generate new mathematical constants… Thus it
cannot be a source for new unique propositions that let you
discriminate between before and after entering the loop? Or?
