On Tuesday, 29 July 2014 at 22:07:42 UTC, Timon Gehr wrote:
> On 07/29/2014 11:08 PM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>> The best you can hope to have is partial correctness. Even with a system
>> for formal verification.
>
> Well, why would this be true?

Because there is no way you can prove say OpenGL drivers to be correct. They are a black box provided by the execution environment.

On Wednesday, 30 July 2014 at 03:32:50 UTC, Walter Bright wrote:
> I don't either. I still have no idea what the difference between assume(i<6) and assert(i<6) is supposed to be.

assert:
is a runtime check of the condition.
is a debugging/correctness checking feature.
is used when the expression is believed true, but is not proven so.
(if it was proven, then there is no purpose in asserting it with a redundant runtime check that is guaranteed to never activate.)

assume:
passes a hint to the optimizer to allow better code generation.
is used when the expression is proven to be true (by the programmer, like @trusted).

The only relation between the two is that if a runtime check for (x) is inserted at some point, it is safe to insert an assume(x) statement afterwards, because x is known true at that point.

If assert degenerates to assume in release mode, any bugs in the program could potentially cause a lot more brittleness and unexpected/undefined behavior than they otherwise would have. In particular, code generation based on invalid assumptions could be memory unsafe.

On 7/30/2014 12:54 AM, David Bregman wrote:
> On Wednesday, 30 July 2014 at 03:32:50 UTC, Walter Bright wrote:
>> I don't either. I still have no idea what the difference between assume(i<6)
>> and assert(i<6) is supposed to be.
>
> assert:
> is a runtime check of the condition.
> is a debugging/correctness checking feature.
> is used when the expression is believed true, but is not proven so.
> (if it was proven, then there is no purpose in asserting it with a redundant
> runtime check that is guaranteed to never activate.)
>
> assume:
> passes a hint to the optimizer to allow better code generation.
> is used when the expression is proven to be true (by the programmer, like
> @trusted).

It still means the same thing as assert.


> The only relation between the two is that if a runtime check for (x) is inserted
> at some point, it is safe to insert an assume(x) statement afterwards, because x
> is known true at that point.

I.e. they're the same thing.


> If assert degenerates to assume in release mode, any bugs in the program could
> potentially cause a lot more brittleness and unexpected/undefined behavior than
> they otherwise would have. In particular, code generation based on invalid
> assumptions could be memory unsafe.

Which is why assert can also do a runtime check.

Walter Bright:

> Data flow analysis can figure that example out.

Sorry, my mistake, what I am discussing about should not need much flow analysis. Here x and y are immutable:


void main(in string[] args) {
    import std.stdio, std.conv;

    assert(args.length == 3);
    immutable ubyte ux = args[1].to!ubyte;
    immutable ubyte uy = args[2].to!ubyte;
    immutable int x = ux;
    immutable int y = uy;

    immutable int result = x * y;
    writeln("Product: ", result);
}


In the current D compiler x and y keep a value range of ubytes (despite they are ints), so here D knows the expression "x * y" can't overflow, so even this is accepted with no casts needed:

immutable ushort result = x * y;



Now let's convert that code with SInt (x and y are still immutable, unlike in my precedent post):


void main(in string[] args) {
    import std.stdio, std.conv, std.experimental.safeintegral;

    assert(args.length == 3);
    immutable ubyte ux = args[1].to!ubyte;
    immutable ubyte uy = args[2].to!ubyte;
    immutable SInt x = ux;
    immutable SInt y = uy;

    immutable SInt result = x * y;
    assert(!result.overflow);
    writeln("Product: ", result);
}


What's I'd like is a way for x and y (that are of the library-defined type SInt) to keep the value range of an ubyte. So the compiler is able to rewrite this:

immutable SInt result = x * y;

removing the call to muls() and replacing it with a regular multiplication, that is faster, even when no inlining happens. (To do this SInt needs two different "instantiations" of its opBinary("*") ).


> If it can't for a more complex one, you can do:
>
>   assert(x >= 0 && x <= 255);
>   assert(y >= 0 && y <= 255);

For such simple situations I don't want user annotations. The only code needed to make this request work should be already written inside the implementation of SInt and similar user-defined types.


And assume() and assert() are two different things, used for different purposes. Do not give the same name to two so different features, if you want to keep a language sane.

Info about assume in Microsoft C++:
http://msdn.microsoft.com/en-us/library/1b3fsfxw.aspx


> The optimizer can certainly use asserts to provide semantic information (even though the dmd one doesn't at the moment).

This is not a good idea. That's the job for assume(), not for assert.

In general assert() verifies something is true, and if it's false, the program just raises an assert error, that is even recoverable. An assert leaves a condition testing inside the binary in debug builds.

An assume() doesn't need to leave a test condition inside the binary, even in debug builds. It doesn't raise run-time errors. It's just a way to tell the compiler that some predicate is true, and the optimization stages of the compiler have to try to use this information to optimize the code.

You can't mix or replace the two things, because a mistake in an assert() doesn't cause your program to burn, it just raises a compile-time error. A programmer mistake in an assume() burns your house.

assert() can be used freely in your code, to make sure you have not done a mistake. assume() is only for special situations where you know something is true, that the compiler can't prove by itself.


> Again, I know you like reading about new languages and language features. I think you'd enjoy that even more supplemented with a book on how compilers work internally, in particular, how data flow analysis works and what it can do.

I will read more about that topic.

Bye,
bearophile

On 7/30/2014 12:17 AM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>[...]

This is a complete misunderstanding of what assert is. Assert means the expression must evaluate to true, if it does not, it's a program bug. This is the case regardless of release mode or not.

On 07/30/14 05:32, Walter Bright via Digitalmars-d wrote:
> 
> I still have no idea what the difference between assume(i<6) and assert(i<6) is supposed to be.

   if (!(i<6)) assert(0); // With the difference that this `assert(0)` could be omitted.

vs

   assert(i<6);


You've been suggesting exposing the assert condition and giving it meaning other than just a harmless debugging check. That would be very dangerous; a wrong assert could change perfectly fine code into a buggy and unsafe one. This is not a theoretical issue:

   bool plain_assert(int i) {
      assert(i<6);
      return i==9;
   }
   bool assert_abused_as_assume(int i) {
      if (!(i<6)) assert(0);
      return i==9;
   }

The second function is already compiled into the equivalent
of `return false;`. (The assert isn't removed, but that's only
because of the `assert(0)` special case; for true asserts it would
be)

`assert` is for *verifying* assumptions. It must not allow them to leak/escape. Otherwise a single not-100%-correct assert could defeat critical runtime checks.

'assume' would be useful, but dangerous, like a reinterpret cast; it would need to be @trusted.

artur

On Wednesday, 30 July 2014 at 09:13:56 UTC, Walter Bright wrote:
> On 7/30/2014 12:17 AM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
>>[...]
>
> This is a complete misunderstanding of what assert is. Assert means the expression must evaluate to true, if it does not, it's a program bug. This is the case regardless of release mode or not.

Yes, that is my argument too. But you claim it isn't. You claim it can be used for optimization as an annotation. Which is flat out wrong.

This discussion will go nowhere until we both agree on what Hoare Logic is capable of and what an annotation can be used for.

O-J. Dahl's book Verifiable Programming is my main reference point. I read it in 3-4 days (before an exam) so it isn't too hard, but there are probably more updated books on the topic. Wikipedia does a fair job.

http://en.wikipedia.org/wiki/Hoare_logic

Allowing assert(0) as an annotation is like allowing assume(true==false). Bearophile is right in disliking the semantics and wanting halt() instead.

D would be much better off taking the direction of HAVOC:

http://research.microsoft.com/en-us/downloads/a6d296dc-e42b-4789-a720-bd3ea7b64487/

Let's try to me more formal about it then.

"assert(X)" means: !(X) || bottom

"assume(X)" means: X

On Wednesday, 30 July 2014 at 10:17:58 UTC, Ola Fosheim Grøstad wrote:
> Let's try to me more formal about it then.
>
> "assert(X)" means: !(X) || bottom
>
> "assume(X)" means: X


Got that wrong (so much for correctness!):

"assert(X)" means: X || bottom

"assume(X)" means: X

Here is a link to the original paper where C.A.R. Hoare introduces assertions. Yes "assert()" in C is the same. The D spec claims to provide C-style assertions. That means it should abide to what is described in this paper:

http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf

If not, call it something else.