assert semantic change proposal

[Timon Gehr via Digitalmars-d]

On 08/09/2014 09:26 PM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= 
<ola.fosheim.grostad+dlang at gmail.com>" 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?