On Tuesday, 29 July 2014 at 06:35:06 UTC, Daniel Murphy wrote:
> The idea is you test your code with assertions enabled, and then only use '-release' when you are sure your program functions correctly.

It never works correctly, until proven correct formally with an automated theorem prover. As I pointed out, even if you only make a mistake in 1 out of 1000 asserts (mistake being having an assert not matching the program logic) you still get a 40% chance of complete failure. No programmer is capable of such a low error rate either.

Please note that is not sufficient for the asserts to follow the specification, they must also not contradiction the logic embedded in the program. One contradictive theorem in the optimizer and it will generate garbage.

For this to work without formal proofs you will have to:

1. do exhaustive unit-testing of all input, function by function.
2. the function has to be fully deterministic (no multi-threading, floats, timers etc)

The key to verifying correctness is that you have 2 separate formulations of the same logic:

1. specification
2. implementation

You compare the implementation to the specification. That is what verifying correctness is.

If you use the specification for implementation (which is what conflating assert() with assume() is), then you only have the implementation and all discrepancies will lead to contradictions or other flaws that will lead to illegal code-gen. And undetected.

This thread gives me an headache… :-(

On Tuesday, 29 July 2014 at 10:40:33 UTC, John Colvin wrote:
> In a correct program (a necessary but not sufficient condition for which is to not violate it's asserts) it is the same.

Define a correct program.

This is a correct program:

S = full specification ( say in prolog or haskell )
P = implementation in an imperative language
A = valid input

TheoremProver( S(x) == P(x) for all x in A )

Yes, in that case you can take any theorems derived from S applied to P and use them for optimization.

In all other cases, injecting theorems more or less randomly into P and then testing them for a small subset of A will never lead to correct theorems pertaining to P. Thus they cannot be used for optimizing P either.

On 7/29/2014 3:13 AM, Dicebot wrote:
> On Tuesday, 29 July 2014 at 07:31:26 UTC, Walter Bright wrote:
>> You can choose to disable assertions with a switch, or not. Having a choice up
>> to you doesn't make it useless.
>
> Yes I know what are options to make it work. I don't know how to make it work
> "in a good style". This is not just D problem - I feel like something is missing
> in the design by contract idea, something that actually can make it robust
> enough to be used without "oh crap" moments.

To have an assert despite -release, you can do things like:

   assert(exp);  =>  if (!exp) assert(0);

I generally leave asserts in for released code in my projects. You can see this in dmd which often exhibits a fault as a tripped assert. But if for nothing else, a way to turn them off gives the developer an easy way to see exactly how much they cost him in performance, so he can make the best decision for his application.

I've also been known to use debug versioning to add a bunch of extra testing code for dev testing.


>> Also, assertions are not for validating user input.
> This is one of problems. When writing library function you don't exactly know if
> input is going to be user input. Use enforces - and it won't be possible to
> optimize away redundant checks. Use assertions and issue may slip uncaught.

It's a serious, serious mistake to use asserts for user input validation. If passing raw user input to a library function, unless that function is specifically documented to validate it, you've made a big mistake.

Asserts are meant to test for logic bugs in the program. Nothing else.


> It feels like for contracts to really work some good implementation of red-green
> code zones is necessarily, to be able to distinguish user input call paths from
> internal ones during compilation time.

That's not what contracts are for (beating a dead horse).

Joel Spolsky made a suggestion I like - have raw user input be of a different type than validated input. That way, functions are clearly and checkably red-green zoned.

On 7/29/14, 12:35 PM, Walter Bright wrote:
> On 7/29/2014 3:13 AM, Dicebot wrote:
>> On Tuesday, 29 July 2014 at 07:31:26 UTC, Walter Bright wrote:
>>> You can choose to disable assertions with a switch, or not. Having a
>>> choice up
>>> to you doesn't make it useless.
>>
>> Yes I know what are options to make it work. I don't know how to make
>> it work
>> "in a good style". This is not just D problem - I feel like something
>> is missing
>> in the design by contract idea, something that actually can make it
>> robust
>> enough to be used without "oh crap" moments.
>
> To have an assert despite -release, you can do things like:
>
>     assert(exp);  =>  if (!exp) assert(0);

Fancier: exp || assert(0) is still an expression.

> I generally leave asserts in for released code in my projects. You can
> see this in dmd which often exhibits a fault as a tripped assert.

I wonder how fast dmd would be if we turned assertions off. Would be an interesting experiment to run.


Andrei

On Tuesday, 29 July 2014 at 10:40:33 UTC, John Colvin wrote:
> On Tuesday, 29 July 2014 at 09:40:27 UTC, Marc Schütz wrote:
>>    assert(a >= 0);
>>    return a < 0;
>>
>> is equivalent to
>>
>>    assert(a >= 0);
>>    return true;
>>
>> but only in non-release mode. In release mode, this effectively becomes
>>
>>    return a < 0;
>>
>> which is _not_ equivalent to
>>
>>    return true;
>>
>> I believe this is was Ola is protesting about, and I agree with him. Such optimizations must only happen if the check stays.
>
> you mean assert(a < 0) or assert(!(a >= 0)) right?

Ah, yes, of course. Alternatively, `return false;`.

>
> In a correct program (a necessary but not sufficient condition for which is to not violate it's asserts) it is the same.
>
> The program is in error if a > 0, whether the assert is compiled in or not. Running in debug mode can simply mean "check my assumptions".

Yes, it only breaks if the program is incorrect. The difference is that it asserts in non-release mode, and just goes on and produces garbage in release mode.

Now, it's of course a valid standpoint to say that your program is going to break anyway, because your assumptions (that you expressed by `assert`) were wrong. But on the other hand, you additionally inserted checks (`a < 0`) to test for it. The above examples are artificial, but in reality these additional checks could be located in an external library, and could have been written by a different author.

It might not be such a good idea to circumvent the checks. In this sense, asserts would indeed make the library code - which might have been completely safe by itself - suddenly unsafe.

Of course, this is only relevant if the compiler first optimizes, and then removes the asserts (in release mode). If it removes the asserts first, and optimizes after, everything is fine.

On 07/29/2014 03:07 AM, Walter Bright wrote:
> On 7/28/2014 1:49 PM, "Ola Fosheim Grøstad"
> <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>> You might want to assert() that you have enough headroom in a statically
>> allocated buffer when testing. Say you assert that the buffer is never
>> more than
>> 50% full for normal loads. You obviously don't want the -release build
>> to make
>> such an assumption!
>
> You're misunderstanding

He still has a point. This is just another case of the keyword not matching the semantics very well. It would be more aptly named 'assume' instead of 'assert' (and be un-@safe if release mode is to trust it unconditionally.)

> and misusing assert.
>
> 'assume' is completely redundant with 'assert'.
> ...

Only if you assume _a priori_ the program to be correct.

> To have different debug builds, use debug statements.

'version(assert) assert' is a better match here, because if one uses 'debug assert', there is the possibility of passing both -debug and -release and get the undesired behaviour.

On Tuesday, 29 July 2014 at 20:07:16 UTC, Timon Gehr wrote:
> He still has a point. This is just another case of the keyword not matching the semantics very well. It would be more aptly named 'assume' instead of 'assert' (and be un-@safe if release mode is to trust it unconditionally.)

But you cannot check preconditions, postconditions and invariants with an assumption!

Assumptions does not have to be checked. They have to be proved. And preferably formally verified. Sure, it might be nice to have 2-5 assumes() in a program to boost optimizers where it fails. Without a proof of correctness? Insane!

Seriously, have anyone EVER read a programming book where all examples worked? And those are tiny toy programs and vetted.

Heck, even Ole-Johan Dahls book on Verifiable Programming, with Hoare as editor had a fairly long errata. And it was carefully written.

Anyway, if you cannot assert() with headroom then you cannot use assert loop invariants in many floating point algorithms.

There are plenty of sources of indeterminism in a real execution environment, so anything more than very limited partial correctness is a pipe-dream for any complex interactive program.

> Only if you assume _a priori_ the program to be correct.

Which is insane. Having 2-3 carefully crafted assume() and 500 assert() would be ok (but I am in doubt of even that). Having 500+ assume() is crazy.

On 07/29/2014 08:54 PM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Tuesday, 29 July 2014 at 10:40:33 UTC, John Colvin wrote:
>> In a correct program (a necessary but not sufficient condition for
>> which is to not violate it's asserts) it is the same.
>
> Define a correct program.
>
> This is a correct program:
>
> S = full specification ( say in prolog or haskell )

(Prolog and Haskell are not particularly natural languages for specification.)

On 7/29/2014 1:07 PM, Timon Gehr wrote:
> On 07/29/2014 03:07 AM, Walter Bright wrote:
>> On 7/28/2014 1:49 PM, "Ola Fosheim Grøstad"
>> <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>>> You might want to assert() that you have enough headroom in a statically
>>> allocated buffer when testing. Say you assert that the buffer is never
>>> more than
>>> 50% full for normal loads. You obviously don't want the -release build
>>> to make
>>> such an assumption!
>>
>> You're misunderstanding
>
> He still has a point. This is just another case of the keyword not matching the
> semantics very well. It would be more aptly named 'assume' instead of 'assert'
> (and be un-@safe if release mode is to trust it unconditionally.)

I find this splitting of hares between assume and assert to be entirely meaningless.


>> and misusing assert.
>>
>> 'assume' is completely redundant with 'assert'.
> Only if you assume _a priori_ the program to be correct.

I've read yours and Ola's explanations of the difference, and I still can't discern any difference, other than the spelling.


>> To have different debug builds, use debug statements.
> 'version(assert) assert' is a better match here, because if one uses 'debug
> assert', there is the possibility of passing both -debug and -release and get
> the undesired behaviour.

That cure sounds worse than the (supposed) problem.


I still have problems convincing people that assert is not to be used to validate user input. Howinell is there any hope of getting anyone to understand all this fine-grained hare-splitting? Heck, I don't see any useful difference between assert and assume.

On 7/29/14, 1:52 PM, Walter Bright wrote:
> I find this splitting of hares ... to be entirely meaningless.

Hunters claim that rabbit tastes less gamey, if we're going to be splitting anything.

(Please forgive the silliness.)