On 08/10/2014 04:40 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?=
<ola.fosheim.grostad+dl...@gmail.com>" wrote:
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
I.e. everything afterwards is unreachable.
⦃ Q ∧ ¬Q ⦄
⦃ false ⦄ // this means 'unreachable'
assert(false); // goes through
implication is not equivalence
Do you agree we indeed have equivalence for those programs with an empty
precondition?
or that it cannot be proved by the the assumptions, hence the assumptions
need strengthening.
...
'false' is the strongest statement. Why would you need to strengthen
assumptions?
(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.
...
If the precondition is actually assumed to hold for all executions of
the program, a precondition of 'false' means that the program never
executes. Maybe you don't assume this, but internally to the logic, this
is what happens: You verify the postcondition under the assumption of
the precondition. I.e. in this case you verify the postcondition of the
program under the assumption that it never executes.
Of course you may still execute such a program, but the ⦃ ⦄ assertions
become irrelevant to this execution.
Note that an optimizer needs to be able to use deduced facts for program
transformations, or it is useless. To an optimizer, a contradiction
means 'unreachable'. There are no non-trivial preconditions (in your
sense, i.e. the program still may have interesting behaviour if they are
violated) on the program used to deduce those facts. Do you agree that
_if_ 'assume' is to be seen as an optimizer hint, then 'assume(false)'
means 'assume unreachable'?
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.
They exist for the virtue of being convenient formalisms for some
applications, but they can be embedded into e.g. set theory just fine.
Deduction lacks a notion of time.
...
What is 'a notion of time' and how does HL provide it?
⦃ P ∧ Q ⦄ // ← precondition
assert(Q); // ← statement
⦃ P ⦄ // ← postcondition
Makes no sense.
It is a definition. If you actually want to understand David's point you
should digest it.
Does
⦃ false ⦄
abort;
⦃ P ⦄
make sense to you?
The assert(Q); statement is equivalent to
if(¬Q) abort;
Assert is not an imperative statement,
Yes, it may be seen to be.
it is an annotation. It is meta.
If it is part of the program it is not 'meta'.
Here, there is a distinction between:
assert(P) // statement
and
⦃ P ⦄ // "meta"
even though both are commonly called 'assertions'.
assert(P); is a statement and hence it needs to be given a semantics,
e.g. an axiomatic semantics or by rewriting, as above.
(BTW: This is not about being right or wrong. It is about understanding
each other's statements in the right context.)
