On 7/30/2014 10:49 PM, Tofu Ninja wrote:
> On Thursday, 31 July 2014 at 05:05:33 UTC, Walter Bright wrote:
>> On 7/30/2014 8:09 PM, Tofu Ninja wrote:
>>> When is the appropriate time to use an assert? If an assert
>>> should not be used on input, then any thing that can't be
>>> statically known is considered an input and anything that is
>>> derived from an input is also an input... so when can we use an
>>> assert? The only things left it seems are things know at compile
>>> time and at that point what is the the point of having assert
>>> when we have static assert...
>>
>> Asserts are used to verify the logic of your code is correct:
>>
>>    x = y + y;
>>    assert(x == 2 * y);
>
> If x and y are floats and y is nan then that assert will fail.....
> That assert is implicitly verifying that the input y is not nan,
> that is a misuse of assert by your definition.

If it pleases you, prepend int x,y; to the snippet.


> Any assert made on a piece of data that is derived from inputs is
> verifying some aspect of that input, which is a misuse of assert
> according to the current definition. So I still state that
> according to current definitions, assert should only be used on
> things that are known at compile time. What is the use of that?

For example, you can have a sort function, and then at the end assert that the output of the function is sorted.

"H. S. Teoh via Digitalmars-d"  wrote in message news:mailman.255.1406747871.16021.digitalmars-d@puremagic.com...

> Wait, what? I thought the whole point of enforce is that it will *not*
> be removed by the compiler, no matter what?

No, the compiler is free to remove it if it can prove it will never be triggered.  eg if the condition is checking a ubyte < 1000.  If the assert in that example is never false, then the enforce is dead code. 

"Daniel Murphy"  wrote in message news:lrct2d$1me8$1@digitalmars.com...

> > Wait, what? I thought the whole point of enforce is that it will *not*
> > be removed by the compiler, no matter what?
>
> No, the compiler is free to remove it if it can prove it will never be triggered.  eg if the condition is checking a ubyte < 1000.  If the assert in that example is never false, then the enforce is dead code.

Actually, thinking about this some more...

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. 

On Wednesday, 30 July 2014 at 18:23:06 UTC, Daniel Murphy wrote:
> "John Colvin"  wrote in message news:oyzjykmvgzdzkprzujzx@forum.dlang.org...
>
>> > Don't use -release.
>>
>> haha yeah, or that!
>
> debug enforce(...) would also work just fine.  It depends if you're happy with leaving bounds checking enabled, if you want fine-grained control over which checks get enabled, if your code needs to be nothrow, etc
>
> I often write quick scripts that rely on bounds checking and assertions to reject incorrect command line args.  While this is technically an abuse of assert, it doesn't matter because I never use -release on them.

version(assert) {} else static assert("This module needs it's assertions");
version(D_NoBoundsChecks) static assert("This module needs it's bounds checking");

On Thursday, 31 July 2014 at 08:23:44 UTC, Daniel Murphy wrote:
> "Daniel Murphy"  wrote in message news:lrct2d$1me8$1@digitalmars.com...
>
>> > Wait, what? I thought the whole point of enforce is that it will *not*
>> > be removed by the compiler, no matter what?
>>
>> No, the compiler is free to remove it if it can prove it will never be triggered.  eg if the condition is checking a ubyte < 1000.  If the assert in that example is never false, then the enforce is dead code.
>
> Actually, thinking about this some more...
>
> 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.

Wait what? Now I'm confused.

x < y is guaranteed at point B (the assert).

x and y are unchanged between point A (the enforce) and point B.

Therefore, x < y is guaranteed at point A

No? Is there some sort of technical limitation?

On Thursday, 31 July 2014 at 08:23:44 UTC, Daniel Murphy wrote:
> "Daniel Murphy"  wrote in message news:lrct2d$1me8$1@digitalmars.com...
>
>> > Wait, what? I thought the whole point of enforce is that it will *not*
>> > be removed by the compiler, no matter what?
>>
>> No, the compiler is free to remove it if it can prove it will never be triggered.  eg if the condition is checking a ubyte < 1000.  If the assert in that example is never false, then the enforce is dead code.
>
> Actually, thinking about this some more...
>
> 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.

No, if assert means "I promise that x < y where assert() is called", then "x < y" also holds when "enforce()" is called, because x and y cannot have changed between the two calls.

On Wednesday, 30 July 2014 at 19:17:51 UTC, H. S. Teoh via Digitalmars-d wrote:
> On Wed, Jul 30, 2014 at 07:09:41PM +0000, via Digitalmars-d wrote:
>> On Wednesday, 30 July 2014 at 18:25:43 UTC, H. S. Teoh via Digitalmars-d
>> wrote:
>> >If you want the check to always be there, use enforce, not assert.
>> 
>> Doesn't help:
>> 
>>     module a;
>>     void bar(int x) {
>>         assert(x > 0);
>>         writeln("x = ", x);
>>     }
>>     // --------
>>     module b;
>>     import a;
>>     void foo(int x) {
>>         enforce(x > 0);
>>         bar(x);
>>     }
>> 
>> If `assert` is treated like `assume` (under Ola's definitions), then
>> `enforce` can be optimized away.
>
> Wait, what? I thought the whole point of enforce is that it will *not*
> be removed by the compiler, no matter what?

Unfortunately not under the current definition of assert :-(

On Thursday, 31 July 2014 at 05:56:31 UTC, Walter Bright wrote:
> On 7/30/2014 10:16 PM, bearophile wrote:
>> Walter Bright:
>>> Show me a piece of code with different behavior. Start with the array bounds
>>> thing.
>> People have already shown you code that behaves differently with assert and
>> assume.
>
> I'd like to see what you are saying is different in a real example.
>
>
>> But you have redefined "assert" to mean a mix of assume and assert.
>
> I haven't redefined anything. It's always been that way. It's used that way in C/C++ (see your Microsoft C++ link).

No.

This is safe:

assert(x) {
   if(!x) halt();
   assume(x);
}

This is not safe:

assert(x){
  assume(x);
}


You need to underestand what can be proven with Hoare logic. The optimizer is free to do anything you can do with it.

A program + libaries contain millions of statements. Each and every of those statements is taken as something close to an axiom or multiple axioms. Basically your program contains millions of implicit assumes() that are internally consistent.

Then you add thousands handwritten axioms of assume().

true == false IFF a single of those axioms contradicts another axiom either provided implicitly by the program/optimizer or explicitly by the user.

That means any boolean expression in your program+libraries can be proven true or false randomly with a probability close to 100%.

That means you cannot do heavy duty optimization at all! Because the probability of no axioms contradicting each other is very close to 0%!

Please note that you can infer true==false if there is even the tiniest teeny weeny sign of contradiction in any pair of axioms picked from the millions upon millions of axioms provided. Even if that axiom is derived from a statement deep down in some library that most likely will never execute.

assume(X) provides axiom X

assert(X) provides theorem(X) to be proven

You cannot mix those two. That is disaster.

Walter Bright <newshound2@digitalmars.com> wrote:
> On 7/30/2014 10:16 PM, bearophile wrote:
>> But you have redefined "assert" to mean a mix of assume and assert.
> 
> I haven't redefined anything. It's always been that way. It's used that way in C/C++ (see your Microsoft C++ link).

Actually I cannot find anything in (the latest draft of) the C standard that would allow that. There's no mention of undefined behavior if an assertion is not met with NDEBUG defined. It's clearly defined what the macro should expnd to in that case.

Quote (Source: http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf):
---
The header <assert.h> defines the assert and static_assert macros and
refers to another macro,
NDEBUG
which is not defined by <assert.h>. If NDEBUG is defined as a macro name at
the point in the source file where <assert.h> is included, the assert macro
is defined simply as
#define assert(ignore) ((void)0)
The assert macro is redefined according to the current state of NDEBUG each
time that
<assert.h> is included.
---
And:
---
The assert macro puts diagnostic tests into programs; it expands to a void expression. When it is executed, if expression (which shall have a scalar type) is false (that is, compares equal to 0), the assert macro writes information about the particular call that failed (including the text of the argument, the name of the source file, the source line number, and the name of the enclosing function — the latter are respectively the values of the preprocessing macros __FILE__ and __LINE__ and of the identifier __func__) on the standard error stream in an implementation-defined format.191) It then calls the abort function.
---

Tobi

Ola Fosheim Grøstad:

> Here is a set of examples of annotated programs that have been formally proved correct for those interested:
>
> http://toccata.lri.fr/gallery/why3.en.html

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

One way to solve this problem: the editor has to show the testing code with a different background color (and collapse it away on request).
(And I'd like to read the "More realistic code with bitwise operations").

-------------------

I have added a third version here:
http://rosettacode.org/wiki/Dutch_national_flag_problem#More_Verified_Version

Adapted from:
http://toccata.lri.fr/gallery/flag.en.html

D lacks the pre-state (old a) and (at a 'Init), the loop variants, the loop invariants (despite D has a invariant keyword used for struct/classe invariants), ghost variables (I have used 'riPred' and 'aInit' for the loop variants and invariants. I have used a debug{} to simulate them in D), and writing the post-condition was a bit of pain.

Bye,
bearophile