On Tuesday, 29 July 2014 at 20:52:28 UTC, Walter Bright wrote:
> I've read yours and Ola's explanations of the difference, and I still can't discern any difference, other than the spelling.

Here is the difference:

action1(cmd){
  assert( !lowercase( cmd )); //wrong theorem
  if(cmd=='format') format_harddisk()
}

action2(cmd){
  assume( !lowercase( cmd )); //wrong theorem
  if(cmd=='format') format_harddisk()
}


release:

action1(cmd){
  if(cmd=='format') format_harddisk()
}

action2(cmd){
  format_harddisk()
}

> I still have problems convincing people that assert is not to be used to validate user input.

Has nothing to do with user input. From a correctness perspective there is no such thing as user input. You only get valid input. What you almost always have is a mismatch between specification and implementation. The best you can hope to have is partial correctness. Even with a system for formal verification.

On Tuesday, 29 July 2014 at 21:08:55 UTC, Ola Fosheim Grøstad wrote:

Sorry, got that wrong (it is late), meant to do this:

lowercase(str){
  if(...){
     assume(str=='format'); // wrong theorem
  }
   ...
}

action1(cmd){
    cmd = lowercase( cmd );
    if(cmd=='format') format_harddisk()
}

action2(cmd) // the same with assert() instead of assume()

release:

action1(cmd){
   cmd = lowercase(cmd);
   if(cmd=='format') format_harddisk()
}

action2(cmd){
   cmd = lowercase(cmd);
   format_harddisk()
}

On 07/29/2014 10:52 PM, Walter Bright wrote:
> 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.
> ...

They are dual concepts. Assert demands a property to hold, assume provides a property that holds.

_According to the previous posts in this discussion_, in release mode, 'assert' provides a property that holds without any demands.

All I was saying is that

1. This particular behaviour is characteristic for an assumption, not an assertion, according to the above characterisation, which is standard in certain communities, like people who are into verification of procedural programs.

2. Code containing such a construct must in general be monitored to ensure memory safety, hence can at most be @trusted.

>
>>> 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.
>
> That cure sounds worse than the (supposed) problem.
> ...

I was just pointing out how to properly prevent optimization based on disabled assertions.

(Unless, of course, you want to tell me a compiler may assume that anything in a version(assert) block can be assumed to actually be part of the program by the optimizer, which is very hard to implement, and may not even make sense in all circumstances.

BTW what about the following gem?

version(assert){}
else int x=2;
assert({
    static if(is(typeof(x))) enum e=loopForever();
    return someExpression;
}());

Should I expect it to stall compilation starting from a certain optimization level in -release mode, or what should be going on here?)

>
> 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.

I hope this post cleared it up a little.

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?

Walter Bright:

> Here there are no new language features required. muls() being an intrinsic means the compiler knows about it. The compiler already does data flow analysis on constants, meaning it knows that x is 100,

Another example program, hopefully more clear:


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;
    SInt x = ux;
    SInt y = uy;

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


Here SInt is a safe integral struct, that overloads the operators like "*" and internally calls muls().

In this program x and y are not constants (like in my original program, but here it's more visible).

What I'd like is the compiler to replace the call to muls() inside the opBinary() of SInt with a simple unsafe integer multiplication because the value range of x and y is [0, 255] for both, so the compiler knows the multiplication can't overflow.

How do you do this with no additional language features?

In my opinion the opBinary() of SInt needs a way to know at compile-time that the range of the two inputs are small enough to not overflow (so opBinary() becomes like a template with two instantiations).

Bye,
bearophile

On 7/29/2014 3:02 PM, Timon Gehr wrote:
> They are dual concepts. Assert demands a property to hold, assume provides a
> property that holds.

A distinction without a difference. potayto, potahto


> 1. This particular behaviour is characteristic for an assumption, not an
> assertion, according to the above characterisation, which is standard in certain
> communities, like people who are into verification of procedural programs.
>
> 2. Code containing such a construct must in general be monitored to ensure
> memory safety, hence can at most be @trusted.

??


> I was just pointing out how to properly prevent optimization based on disabled
> assertions.

??


> (Unless, of course, you want to tell me a compiler may assume that anything in a
> version(assert) block can be assumed to actually be part of the program by the
> optimizer, which is very hard to implement, and may not even make sense in all
> circumstances.

I don't know what you're assuming (!) the version(assert) even does, as it is not a language feature.


> BTW what about the following gem?
>
> version(assert){}
> else int x=2;
> assert({
>      static if(is(typeof(x))) enum e=loopForever();
>      return someExpression;
> }());
>
> Should I expect it to stall compilation starting from a certain optimization
> level in -release mode, or what should be going on here?)

??


> I hope this post cleared it up a little.

Not a bit. The distinction utterly escapes me.

On 7/29/2014 4:03 PM, bearophile wrote:
> How do you do this with no additional language features?

Data flow analysis can figure that example out. If it can't for a more complex one, you can do:

  assert(x >= 0 && x <= 255);
  assert(y >= 0 && y <= 255);

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


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.

On 07/30/2014 02:48 AM, Walter Bright wrote:
> On 7/29/2014 3:02 PM, Timon Gehr wrote:
>> They are dual concepts. Assert demands a property to hold, assume
>> provides a
>> property that holds.
>
> A distinction without a difference.

Wtf.

(Imagine you are arguing with someone who keeps claiming that the distinction between @trusted and @safe is meaningless and you are roughly in my position.)

> potayto, potahto
> ...

potato.

>
>> 1. This particular behaviour is characteristic for an assumption, not an
>> assertion, according to the above characterisation, which is standard
>> in certain
>> communities, like people who are into verification of procedural
>> programs.
>>
>> 2. Code containing such a construct must in general be monitored to
>> ensure
>> memory safety, hence can at most be @trusted.
>
> ??
> ...

Undefined behaviour does not preserve memory safety.

>
>> I was just pointing out how to properly prevent optimization based on
>> disabled
>> assertions.
>
> ??
> ...

Maybe you weren't following the discussion. What do you think this discussion is about?

On 07/28/2014 03:31 PM, Daniel Murphy wrote:
> "Ola Fosheim Grøstad" " wrote in message
> news:vqlvigvgcplkuohudsju@forum.dlang.org...
>
>> Please guys, you should not change code-gen based on asserts. They are
>> not proofs, they are candidates for formal verification of
>> correctness. They are in essence embedded break-point checks. If you
>> allow asserts to affect codegen then it becomes a very unsafe feature.
>> It's like having a undetected bug in a unit-test introduce bugs in the
>> released program. 8-I
>
> The compiler is allowed to not check assertions in release mode.  This
> is because a program that would fail an assertion is a broken program,
> and by specifying -release you are telling the compiler to assume all
> assertions pass.  I don't see any reason the compiler shouldn't be
> allowed to change code-gen based on asserts.
> ...

This is what spawned this subthread. Does this clear up your question marks?

>
>> (Unless, of course, you want to tell me a compiler may assume that
>> anything in a
>> version(assert) block can be assumed to actually be part of the
>> program by the
>> optimizer, which is very hard to implement, and may not even make
>> sense in all
>> circumstances.
>
> I don't know what you're assuming (!) the version(assert) even does, as
> it is not a language feature.
> ...

Of course version(assert) is a language feature. Always double-check your claims.

It's even documented: http://dlang.org/version.html

>...
>
>> I hope this post cleared it up a little.
>
> Not a bit. The distinction utterly escapes me.

This is unfortunate, but I don't know what else to say.

On 7/29/2014 7:08 PM, Timon Gehr wrote:
> Of course version(assert) is a language feature. Always double-check your claims.
>
> It's even documented: http://dlang.org/version.html

You're right. My mistake. I'd forgotten about that.


>> Not a bit. The distinction utterly escapes me.
> This is unfortunate, but I don't know what else to say.

I don't either. I still have no idea what the difference between assume(i<6) and assert(i<6) is supposed to be.

On Wednesday, 30 July 2014 at 03:32:50 UTC, Walter Bright wrote:
> On 7/29/2014 7:08 PM, Timon Gehr wrote:
>> Of course version(assert) is a language feature. Always double-check your claims.
>>
>> It's even documented: http://dlang.org/version.html
>
> You're right. My mistake. I'd forgotten about that.
>
>
>>> Not a bit. The distinction utterly escapes me.
>> This is unfortunate, but I don't know what else to say.
>
> I don't either. I still have no idea what the difference between assume(i<6) and assert(i<6) is supposed to be.

main(){
  foobar();
  assert(false==true)
}

With assert():

main(){
  foobar();
}

With assume() the optimizer can:

a: proven_locally(main, (false==true))
no_local_dependencies(a)
all_paths_go_through(a)
b: proven_globally(false==true)
for_all_conditional_expressions_try_to_prove_false()

At this point all conditionals are false and removed.
Complete wipe out. Nothing remains.

here's another version:

foo(){
   assume(true==false);
}

version(RELEASE_MODE){
   foobar(){ foo(); }
}
...

main(){
  foobar();
}