On 08/09/2014 09:26 PM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?=
<[email protected]>" wrote:
On Thursday, 7 August 2014 at 23:13:15 UTC, David Bregman wrote:
and use unreachable() if you know 100% it holds.
This is just another name for the same thing, it isn't any more or
less dangerous.
Of course it is. unreachable() could lead to this:
f(){ @unreachable}
g(){...}
f:
g:
machinecode
assume(false) just states that the post condition has not been
proved/tested/verified yet. That does not signify that no code will
reach it.
Formally, that's what it assumes to be the case. If you can prove
'false', this means that the code is unreachable.
if(Q){
⦃ Q ⦄
if(¬Q){
⦃ Q ∧ ¬Q ⦄
⦃ false ⦄ // this means 'unreachable'
assert(false); // goes through
}
}
After assuming 'false' you can prove false.
⦃ false ⦄ still means 'unreachable' if it is 'assume'd.
(Yes, of course it can also be read as 'inconsistent', if the code is
actually reachable, but proving code 'unreachable' which can actually be
reached also just means that the reasoning and the assumptions were
'inconsistent'. You can also read 'inconsistent' as: 'this program will
never actually be executed', etc. David's interpretation of the
formalism is adequate.)
Encouraging assume(false) sounds like an aberration to me.
If you accept my definition of assume there is no problem with it,
it just means unreachable. I showed how this follows naturally from my
definition.
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.
Hoare Logic deals with triplets: precondition, statement, postcondition.
(assume,code,assert)
'assume' and 'assert' are "statement"s:
⦃ P ∧ Q ⦄ // ← precondition
assert(Q); // ← statement
⦃ P ⦄ // ← postcondition
'assume' is just a dual concept:
⦃ P ⦄ // ← precondition
assume(Q); // ← statement
⦃ P ∧ Q ⦄ // ← postcondition
There is nothing 'lacking' here, right?
