On Wednesday, 6 August 2014 at 00:47:28 UTC, Walter Bright wrote:
> On 8/3/2014 7:26 PM, Tove wrote:
>> It is possible, just not as a default enabled warning.
>>
>> Some compilers offers optimization diagnostics which can be enabled by a switch,
>> I'm quite fond of those as it's a much faster way to go through a list of
>> compiler highlighted failed/successful optimizations rather than being forced to
>> check the asm output after every new compiler version or minor code refactoring.
>>
>> In my experience, it actually works fine in huge projects, even if there are
>> false positives you can analyse what changes from the previous version as well
>> as ignoring modules which you know is not performance critical.
>
> If you build dmd in debug mode, and then run it with -O --c, it will give you a list of all the data flow transformations it does.
>
> But the list is a blizzard on non-trivial programs.
What about making a diff file? Or are the transformations so deep that it would be impossible to link them to lines in the source code?

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. It just means that the returned value is uncertain. It does not mean that the code will never be executed.

It is also dangerous to mix them up since CTFE can lead to assume(false). If you want safety and consistence you need to have a designated notation for @unreachable.

>> 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.

>> You need to provide proofs if you attempt using assume(X) and assert(false).
>
> There is no mechanism for providing proofs or checking proofs in D.

Actually, unit tests do. D just lacks the semantics to state that the input accepted by the precondition has been fully covered in unit tests.

> Well, any correct mathematical formalism of the code must preserve its semantics, so it doesn't really matter which one we talk about.

Preserve the semantics of the language, yes. For pure functions there is no difference. And that is generally what is covered by plain HL. The code isn't modified, but you only prove calculations, not output.

> Different lines (or basic blocks, I guess is the right term here) can have different reachability, so you could just give each one its own P.

"basic blocks" is an artifact of a specific intermediate representation. It can cease to exist. For instance MIPS and ARM have quite different conditionals than x86. With a MIPS instruction set a comparison is an expression returning 1 or 0 and you can get away from conditionals by multiplying successive calculations with it to avoid branch penalties. This is also a common trick for speeding up SIMD…

Hoare Logic deals with triplets: precondition, statement, postcondition.  (assume,code,assert)

You start with assume(false), then widen it over the code until the assert is covered for the input you care about.

>> P1 and P2 are propositions, so what are the content of those? The ones you use for your P1=>X and P2=>Y?
>
> This is just an implementation detail of the compiler. Probably each basic block has its own P, which is conservatively approximated with some data flow analysis. (Disclaimer: I am not a compiler expert)

Oh, there is of course no problem by inserting a @unreachable barrier-like construct when you have proven assume(false), but it is a special case. It is not an annotation for deduction.

> Anyways, I don't have much more time to keep justifying my definition of assume. If you still don't like mine, maybe you can give your definition of assume, and demonstrate how that definition is more useful in the context of D.

assume(x) is defined by the preconditions in Hoare Logic triplets. This is what you should stick to for in(){} preconditions.

A backend_assume(x) is very much implementation defined and is a precondition where the postconditions is:

program(input) == executable(input) for all x except those excluded by backend_assume.

However an assume tied to defining a function's degree of verification is not a backend_assume.

That is where D risk going seriously wrong: conflating postconditions (assert) with preconditions (assume) and conflating local guarantees (by unit tests or proofs) with global optimization and backend mechanisms (backend_assume).

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

On 8/7/2014 2:29 AM, Daniel Murphy wrote:
> And we've also got asserts in pre-conditions, which are recoverable by definition.

Pre-condition asserts are not recoverable.

On 8/7/2014 10:44 AM, Daniel Murphy wrote:
> I meant asserts in pre-conditions when used with inheritance.  It's a pass if
> any of the preconditions pass, so the compiler runs them in turn and catches all
> but the last.

That's right, they are OR'd together.

On Sat, Aug 09, 2014 at 05:54:21PM -0700, Walter Bright via Digitalmars-d wrote:
> On 8/7/2014 10:44 AM, Daniel Murphy wrote:
> >I meant asserts in pre-conditions when used with inheritance.  It's a pass if any of the preconditions pass, so the compiler runs them in turn and catches all but the last.
> 
> That's right, they are OR'd together.

Which is fine if they are evaluated as a single expression. The problem right now is that the OR is simulated by catching AssertErrors, which by definition only happens when the program in an invalid state, so the fact that this works at all is only a "lucky coincidence". :-(  If you're "not so lucky" you end up catching a genuine program bug but ignoring it because the other condition in the simulated OR turned out to pass. This unfortunately puts DbC in D on rather shaky ground.


T

-- 
Кто везде - тот нигде.

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.

On 8/9/2014 5:52 PM, Walter Bright wrote:
> On 8/7/2014 2:29 AM, Daniel Murphy wrote:
>> And we've also got asserts in pre-conditions, which are recoverable by
>> definition.
>
> Pre-condition asserts are not recoverable.
>

Eh, ignore that.

On 08/10/2014 04:40 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= <ola.fosheim.grostad+dlang@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.)

On Sunday, 10 August 2014 at 13:47:45 UTC, Timon Gehr wrote:
>> No, if you prove false that means either that it is nonterminating
>
> I.e. everything afterwards is unreachable.

Depends on your take on it. If you support non-deterministic computations (e.g. Ada's "select") then non-termination is treated like bottom. So you can have

infinite_recursion() or terminates() => terminates()

So unreachable in terms of machine-language, sure, but not in terms of execution flow.

> Do you agree we indeed have equivalence for those programs with an empty precondition?

You mean "false" or "true"?

>> 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?

If you succeed in proving the postcondition to be false then the postcondition does not hold and you have to strengthen the precondition or else the triplet is invalid/incorrect. If the precondition is defined false then the postcondition is not required to hold. It is not covered by the proof/verification/specification and the triplet is valid/provably correct.

So if the precondition is defined false then the program is a priori proved correct to the specification, i.e. the specification does not require any guarantees for the result.

> If the precondition is actually assumed to hold for all executions of the program, a precondition of 'false' means that the program never executes.

That is the responsibility of the caller. It is the caller's responsibility to uphold the precondition in order to get guaranteed results.

But you could have multiple pairs of preconditions/postconditions. E.g. you could for a generic function have different pairs for int/float/double or have a separate pair for termination, etc. Or have one set that specifies what is covered by unit-tests, what is vetted by review, what is totally unknown… You could have different types of guarantees for a library and users could take advantage of it based on the requirements for the application (high security vs computer game).

> 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.

It is not always possible to prove termination, so that would be unfortunate. It would be more useful to be able to restrict the precondition to what you cover by unit-tests. Or to have multiple sets of pre/postconditions (proven-by-machine vs vetted-by-review).

Then if you can prove that the caller fulfills the precondition you are able to optimize based on the pre/post condition and assume the post-condition if it is machine-verified.

That would give new optimization possibilities.

That does not mean that you should never be able to use a function outside the verified range (by machine proof), but then you need to assert the results at runtime if you want verified correctness.

> Of course you may still execute such a program, but the ⦃ ⦄ assertions become irrelevant to this execution.

Not really, they could still trap.

> 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'.

No, to an optimizer a contradiction means "all bets are off for the postcondition to hold":

program(x) != executable(x)

That is why __assume(P) must always hold on any reachable path (e.g. any path that the optimizer considers to be a target for optimization).

But __assume is not a regular precondition, it has a counterpart in the optimization invariant (postcondition):

program(x) == executable(x), x not creating contradictions by __assume(…)

The optimizer is presuming that anything goes as long as this optimization invariant can be upheld. This is not a postcondition specified by the programmer at the meta-level. It is implicit.

And the optimizer does not check the implicit precondition, at all…

> to deduce those facts. Do you agree that _if_ 'assume' is to be seen as an optimizer hint, then 'assume(false)' means 'assume unreachable'?

No. I think the optimizer should only use assumptions when they are guaranteed to hold by the caller or the language axioms. Or in the rare case by other machine verifiable axioms (specifications for hardware registers etc).

>> 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.

Not sure what you mean by this and how this relates to imperative programming.

>> Deduction lacks a notion of time.
>> ...
>
> What is 'a notion of time' and how does HL provide it?

It doesn't. Which is why it trips when you don't prove termination. But HL does not do program transformations.

> The assert(Q); statement is equivalent to
>
> if(¬Q) abort;

Not if assert() is considered meta-level. However, since a triplet is tied to an entity/function/module, it would be ok to throw an exception as long as it isn't caught in the module covered by the pre/postcondition triplet if it does not have any side effects.

If you don't reach the postcondition it does not matter.

>> Assert is not an imperative statement,
>
> Yes, it may be seen to be.

That would be an aberration, because the specification should either be independent of the implementation or generate the implementation…

If the specification is considered part of the program then you will run into problems if there are contradictions.

> assert(P); is a statement and hence it needs to be given a semantics, e.g. an axiomatic semantics or by rewriting, as above.

Well, in C it is a statement by implementation, but it is always meant to not have side effects and one should be able to compile with NDEBUG with no difference in program behaviour. So, even though it is implemented as a macro it has always had the status of an annotation.

> (BTW: This is not about being right or wrong. It is about understanding each other's statements in the right context.)

I think the whole game changes when Walter wants to optimize based on the annotations… Then you need to be very careful unless you want to amplify bugs rather than improve the overall performance of the program (speed + correct behaviour).

So then the distinction between specification and implementation, proven and vetted, becomes even more important.

Since D has unit tests as a formalism, then it would be a shame to not use it to verify contracts in a way that could provide safe optimization possibilities rather than relying on programmers being able to write provably correct code in a predictable manner, which just ain't gonna happen.