On Thursday, 31 July 2014 at 20:24:09 UTC, Walter Bright wrote:
> In closing, Hoare's paper:
>
>    http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf
>
> speaks of "assertions" which can be proven to be true. (It doesn't mention "assumptions".) The simplest way to prove it is to put in a runtime check. D's assert() nicely fits in with that.

Assumptions are axioms. It mentions axioms.

This is an axiom:

int x = 0;

On 7/31/14, 12:37 PM, Daniel Gibson wrote:
>
> This thread however shows that many D users (who probably have more D
> experience than myself) are not aware that assert() may influence
> optimization and would prefer to have separate syntax to tell the
> optimizer what values he can expect.

Yah, I think that's a good outcome. We must document assert better. -- Andrei

On Thursday, 31 July 2014 at 20:24:09 UTC, Walter Bright wrote:
> On 7/31/2014 4:36 AM, bearophile wrote:
>> int max(in int x, in int y) {
>>     assume(x > y);
>>     return (x > y) ? x : y;
>> }
>>
>> The optimizer is free to replace that code with this, even in debug builds:
>>
>> int max(in int x, in int y) {
>>     return x;
>> }
>
> That implies that the behavior is undefined if the assumption is false. A compiler is free to add checks for undefined behavior (you yourself are a huge proponent of this) and people would (very reasonably for a quality implementation) expect that the assumption is checked. Hence, it will behave like assert.

You are asking bearophile to give an example, he gives an example, and you redefine his definition?!

The whole point of assume is that it is unchecked and unsafe.

On Thursday, 31 July 2014 at 20:57:10 UTC, Andrei Alexandrescu wrote:
> On 7/31/14, 12:37 PM, Daniel Gibson wrote:
>>
>> This thread however shows that many D users (who probably have more D
>> experience than myself) are not aware that assert() may influence
>> optimization and would prefer to have separate syntax to tell the
>> optimizer what values he can expect.
>
> Yah, I think that's a good outcome. We must document assert better. -- Andrei

Its a little too late for that I think, asserts are already being used so to change the meaning now is wrong. Earlier I said that maybe a documentation change is all that is needed but I retract that statement.

On Thursday, 31 July 2014 at 20:24:09 UTC, Walter Bright wrote:
> On 7/31/2014 4:36 AM, bearophile wrote:
>> (The problem is that your have defined your own idea,
>
> "My" idea is the conventional one for assert - see the Wikipedia entry on it.

That entry makes no mention of assert being used as an optimization hint.

Am 31.07.2014 22:57, schrieb Andrei Alexandrescu:
> On 7/31/14, 12:37 PM, Daniel Gibson wrote:
>>
>> This thread however shows that many D users (who probably have more D
>> experience than myself) are not aware that assert() may influence
>> optimization and would prefer to have separate syntax to tell the
>> optimizer what values he can expect.
>
> Yah, I think that's a good outcome. We must document assert better. --
> Andrei

You should have done so 10 years ago.. experienced D coders (that don't follow this discussion) probably won't look up what exactly assert() does again and and code will silently break in subtle ways once the optimizer uses assert()


But if you (as in "the D language implementors") *really* decide to stick to this unexpected meaning of assert(), you should indeed document this as soon as a proper definition of what assert() does and might do in the future, when enforce() vs assert() should be used.

Maybe, besides enforce() and assert() there could be a check() that:
* returns true if the condition is true
* throws an exception in debug mode if the condition is false
* returns false in release mode if the condition is false
could be introduced.
It could be used like

if(check(x !is null, "x must not be null")) {
	// .. do something with x ..
}

to cater the usecase of "in debugmode I want to know about this problem/behavior immediately to debug it, but in releasemode I want to handle it gracefully".

Cheers,
Daniel

On Thursday, 31 July 2014 at 20:24:09 UTC, Walter Bright wrote:
> Code that relies on assertions being false is semantically broken.

Code transforms that relies on unproven theorems to be true are semantically broken.

Assertions are proposed theorems.

Assumptions are preconditions needed for those theorems.

The contract is not fulfilled until the theorems are proven. PROVEN, not tested by sampling. Until then programming by contract (as defined) requires testing under execution, not only in debug builds.

If you don't do this, then don't call it programming by contract!


You should also then require the following:

"supplier B guarantees postcondition of B's methods assuming client A guarantees the preconditions of those methods"

http://www.cs.usfca.edu/~parrt/course/601/lectures/programming.by.contract.html

So you need this structure:

A(){
   assert(B_preconditions); // try to optimize these away
   B();
   assume(B_postconditions); // not required, but useful for optimization
}

B(){
   assume(B_preconditions)
   …execute…
   assert(B_postconditions) // try to get rid of this through formal proof
}

On 7/31/14, 2:11 PM, Daniel Gibson wrote:
> Maybe, besides enforce() and assert() there could be a check() that:
> * returns true if the condition is true
> * throws an exception in debug mode if the condition is false
> * returns false in release mode if the condition is false
> could be introduced.

Yah, an extra non-magic function that performs the "mild assert" discussed in this thread would be a possibility. -- Andrei

On 07/31/2014 01:32 PM, bearophile wrote:
>
> More comments:
>
> -------------------
>
> A problem with code like this is that it's drowing in noise. The
> precondition/invariant/variant code in the 't3' function is obscuring
> what the code is actually doing on the data:
> http://toccata.lri.fr/gallery/queens.en.html

It is not an inherent issue with verification. One way to avoid this is to allow correctness proofs to be done in a separate place.

On 07/31/2014 10:24 PM, Walter Bright wrote:
>
> Code that relies on assertions being false is semantically broken.
> ...

The code might not rely on it. I.e. the assertion might be the only thing that is broken. Turning it into an assumption will additionally break the code.

> In closing, Hoare's paper:
>
> http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf
>
> speaks of "assertions" which can be proven to be true. (It doesn't
> mention "assumptions".) The simplest way to prove it is to put in a
> runtime check. D's assert() nicely fits in with that.

EWD liked to say things like:
'The first moral of the story is that program testing can be used very effectively to show the presence of bugs but never to show their absence.'.

Which is pedantically speaking obviously wrong without further qualification, but he still has a point.

A non-exhaustive sequence of assertion checks will not be sufficient to prove that the assertion is true. However, turning the assertions into assumptions is valid only if the assertions are true.

Even more importantly, to assume true without proof is very much a different operation than to assert true, for proof (or disproof!) to come later, and 'assert' awkwardly plays both roles if -release may optimize based on it.