On Saturday, 9 August 2014 at 20:22:36 UTC, Timon Gehr wrote:
Formally, that's what it assumes to be the case. If you can
prove 'false', this means that the code is unreachable.
No, if you prove false that means either that it is
nonterminating or that it cannot be proved by the the
assumptions, hence the assumptions need strengthening.
⦃ Q ∧ ¬Q ⦄
⦃ false ⦄ // this means 'unreachable'
assert(false); // goes through
implication is not equivalence
After assuming 'false' you can prove false.
⦃ false ⦄ still means 'unreachable' if it is 'assume'd.
False only means that the postcondition does not hold. If the
precondition is false then the triplet is valid i.e. correct.
(Yes, of course it can also be read as 'inconsistent', if the
code is actually reachable, but proving code 'unreachable'
No, you can have this:
main(){
Precondition(false)
Stuff()
Postcondition(anything)
}
This states that Stuff has not yet been verified for any input.
It does not state that Stuff will never execute.
Your "definition" is lacking. It mixes up two entirely
different perspectives,
the deductive mode and the imperative mode of reasoning.
I think you should elaborate on this a little if you want to
make a point. E.g. I don't think that such an opposition of
'reasoning modes' even exists.
Of course it does, that is why Hoare Logic and SSA exist.
Deduction lacks a notion of time.
⦃ P ∧ Q ⦄ // ← precondition
assert(Q); // ← statement
⦃ P ⦄ // ← postcondition
Makes no sense. Assert is not an imperative statement, it is an
annotation. It is meta.
