On 7/31/2014 1:18 AM, Daniel Murphy wrote:
> In this program the enforce can be removed
>
> assert(x < y);
> enforce(x < y);
>
> But not in this one:
>
> enforce(x < y);
> assert(x < y);
>
> because the compiler does need to take control flow into account when applying
> the information in the assert.  In this case the assert does not actually give
> the compiler any new information.

http://imgur.com/gallery/hzaJ4Hn

On 7/30/2014 4:56 AM, Daniel Murphy wrote:
> If your assertions are invalid and
> you're compiling with -release, the compiler is free to generate invalid code.
> -release is dangerous.  -release is telling the compiler that the code you wrote
> is correct,  and it can rely on it to be correct.

Yes.

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

Let me try:

"assert() expresses a contract that must be true at that point for the program to continue correctly.

Compiler (and the optimizer therein) will generate code that works as intended as long as these contracts are true.

While in Debug mode code for checking the validity of contracts is actually generated and failure of contracts will result in halting the program, in Release mode the code is no longer (guaranteed to be) generated and this results in undefined behavior.

assert(0) is a special contract that requires no code for its verification, as it obviously fails. This is why the compiler will always make it a halting point, in all builds."

On Friday, 1 August 2014 at 02:44:51 UTC, Walter Bright wrote:
>> That entry makes no mention of assert being used as an optimization hint.
>>
> Saying that a predicate is always true means it's available to the optimizer.

An assert does not say that the predicate is always true. It says that this is a theorem to be proven true given the assumptions provided up till that point.

If you:

1. have a set of preconditions (assumptions)
2. and a fully specified postcondition
3. and the code between has no sideeffects
4. and the postcondition has been proven true

Only then can you use the postcondition to eliminate code that was unneccessary to prove the postcondition from the precondition.

So yes, you CAN use asserts to do heavy duty optimization that go way beyond what a regular optimizer can do (even in theory), but not a priori.

In theory you can reduce a general algorithm that does too much work down to the specifics of the postcondition. Doing this for an imperative language is not realistic today.


DESIGN BY CONTRACT

Design by contract does not mean that programmers guarantee the postconditions. Quite the opposite!

Design by contract assumes 3 roles:

1. the trusted ARCHITECT who specifies the modules and pre/postconditions

2. the distrusted IMPLEMENTORS who write the code and cannot touch the contract

3. the trusted BUILD SYSTEM who guarantees that the contracts are upheld between modules, either by proof of run time checks that takes place before one module get access to another.


Claiming that the programmer guarantee asserts to hold true is not design by contract.

Claiming that the build system is responsible for upholding the contract despite programmers doing their utmost to break it is Design by contract.

On Friday, 1 August 2014 at 02:46:48 UTC, Walter Bright wrote:
> On 7/31/2014 1:36 PM, Tofu Ninja wrote:
>> On Thursday, 31 July 2014 at 19:12:04 UTC, Walter Bright wrote:
>>> Integers are sortable, period. That is not "input".
>>
>> Ok so sorted ints are not "input", what else is not "input"? Where can I draw
>> the line? And if I do use assert on an input, that is what? Undefined? I thought
>> D was not supposed to have undefined behavior.
>
> I've answered this so many times now, I no longer have any new words to say on the topic.

I'll say some word on this, then.

Yes, you cannot assert() that input has a specific value. Programs that do this are provable not correct.

You can assert() that input has a specific value after the code has made sure that it has a specific value. This means the program is partially correct.

Input is a priori assumed to have any value allowed by the context.
Argc has an implicit assume that provides axioms describing the limits of int/C/unix/etc.

On Friday, 1 August 2014 at 06:24:29 UTC, Ola Fosheim Grøstad wrote:
> DESIGN BY CONTRACT

BTW, there is an emerging field "program synthesis" that is based on Design by contract where the compiler automatically generates code that takes you from preconditions to postconditions and verifies it to be correct.

Genetic progamming does the same.

That's nice. Now you don't need those annoying programmers that cannot get things right. You only need the architect and the build system.

On Friday, 1 August 2014 at 03:17:06 UTC, Walter Bright wrote:
>>> In fact, the whole reason assert is a core language feature rather than
>>> a library notion is I was anticipating making use of assert for
>>> optimization hints.
>>
>> So why is this not documented?
>
> Frankly, it never occurred to me that it wasn't obvious. When something is ASSERTED to be true, then it is available to the optimizer. After all, that is what optimizers do - rewrite code into a mathematically equivalent form that is provably the same (but cheaper to compute). Its inputs are things that are known to be true.
>
> For example, if a piece of code ASSERTS that x is 3, thereafter the optimizer knows that x must be 3. After all, if the optimizer encounters:
>
>    x = 3;
>
> do I need to then add a note saying the optimizer can now make use of that fact afterwards? The use of "assert" is a very strong word, it is not "maybe" or "possibly" or "sometimes" or "sort of".
>
> When you write:
>
>    assert(x == 3);
>
> then at that point, if x is not 3, then the program is irretrievably, irredeemably, undeniably broken, and the default action is that the program is terminated.
>
> The idea expressed here by more than one that this is not the case in their code is astonishing to me.

This is enough to convince me.

assert - in D - is for documenting assumptions and checking them in non-release builds. It's a reasonable definition - if unexpected to some - and allows good optimisation opportunities.


Do these guidelines sound reasonable:


Don't want the optimiser to use the information from your asserts when the asserts are gone?

Wrap them in a version block and version them out in your release builds. Write a wrapper for assert that does this if you like. You could even write a no-op wrapper for assert and call it assume, if you really want to.


Don't want your defensive checks to ever be removed from a certain bit of code?

Use std.exception.enforce or, if you really insist on assert, put a

version(assert) {} else
    static assert(false, "Must be compiled with assertions enabled");

in the relevant place to prevent people accidentally disabling them.

John Colvin:

> This is enough to convince me.

Please don't feed Walter.

Bye,
bearophile

On 7/31/2014 11:24 PM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Friday, 1 August 2014 at 02:44:51 UTC, Walter Bright wrote:
>>> That entry makes no mention of assert being used as an optimization hint.
>>>
>> Saying that a predicate is always true means it's available to the optimizer.
>
> An assert does not say that the predicate is always true.

Yes, it does. From Meyers' comprehensive tome on the topic "Object-Oriented Software Construction" (1997) where he writes:

"A run-time assertion violation is the manifestation of a bug in the software."

    -- pg. 346

In fact, Meyers calls it "rule (1)" of assertions.

On 8/1/2014 1:31 AM, John Colvin wrote:
> Don't want the optimiser to use the information from your asserts when the
> asserts are gone?

You can always do:

   version(assert) { if (!exp) halt(); }

and in -release mode, the compiler won't assume that exp is true. Or, more simply, just write your own myAssert() template. The compiler won't recognize it as special, it will just be ordinary code with ordinary behavior as the implementor wrote it. There's nothing difficult about it.