On Thu, Jul 31, 2014 at 09:37:11PM +0200, Daniel Gibson via Digitalmars-d 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.
[...]

AFAIK, the compiler currently doesn't use assert as a source of information for optimization, it's just being proposed.


T

-- 
Blunt statements really don't have a point.

Walter Bright:

> That's the way assert in C/C++ conventionally worked. But this is changing. Bearophile's reference made it clear that Microsoft C++ 2013 has already changed,

I am against the idea of turning asserts into a dangerous assert-assume hybrid. And you have ignored some answers by Timon and others.

Bye,
bearophile

Am 31.07.2014 21:46, schrieb H. S. Teoh via Digitalmars-d:
> On Thu, Jul 31, 2014 at 09:37:11PM +0200, Daniel Gibson via Digitalmars-d 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.
> [...]
>
> AFAIK, the compiler currently doesn't use assert as a source of
> information for optimization, it's just being proposed.


Walter said that he implemented assert() as a language feature to allow this, so it's at least planned.
And, as I wrote, if this was/is planned, people should have been told about it *explicitly* in the language documentation, so they can make sure to use assert() accordingly.

Cheers,
Daniel

Daniel Gibson:

> so they can make sure to use assert() accordingly.

What's the correct way to use the assert-assume hybrid?

Bye,
bearophile

On Thursday, 31 July 2014 at 11:32:11 UTC, bearophile wrote:
> 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

Yes, if the algorithm is a bit involved it becomes complicated. It is also expensive to get right, $100-$1000 per line of code?

However, simple stuff that you often have in a standard library is usually easier on the eyes and easier to get right:

http://toccata.lri.fr/gallery/power.en.html

So, having a formally proven standard library would be quite within reach. And if you also have inlining + assume() you could do stuff like this

inline uint floor_sqrt(long x){
   assert(x>=0);
   uint r = _proven_floor_sqrt(x);
   assume(r<=x*x);
   assume( (r>(x-1)*(x-1)) || x==0 );
   return r
}

Precompiled library:

uint _proven_floor_sqrt(long x){
   assume(x>=0); // not test necessary, use this for optimization
   return ...
}

Another nice thing is that you can replace _proven… with handwritten machine language that has been exhaustively tested (all combinations) and still let the compiler assume() the postconditions with no runtime cost.

Another area where assume() is useful is for reading hardware registers that are guaranteed to have certain values so no runtime check is needed:

auto x = read_hw_register(123456);
assume( x==0 || x==1 || x==4 );

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

Thanks, I like the way you go about this. Experimenting with the syntax this way.

> 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),

Yeah, I also think having invariant() in loops makes for more readable code than assert/enforce.

I imagine that you could specify a reduced set of D and do this:

D-source => machinetranslate => prover-source

prover-source => prover => proof-source

proof-source + prover-source => machinetranslate => D-source w/assume() etc


Btw, here is an example of an open source operating system kernel vetted against a haskell modell of the kernel:

http://sel4.systems/
https://github.com/seL4/seL4/tree/master/haskell

So, this formal correctness support in one way or another is clearly a valuable direction for a system level programming language.

On Thursday, 31 July 2014 at 13:37:42 UTC, Daniel Gibson wrote:
> Because (in C/C++) assertions just vanish when NDEBUG isn't defined, it would never occur to me that they have any influence on such (release mode) builds.

Yes, all standards require this for good reason. I don't know why Walter and Andrei thinks conforming C  can do anything else than ignoring assert in release builds:

«
If NDEBUG is defined as a macro name before the inclusion of this header, the assert() macro shall be defined simply as:

#define assert(ignore)((void) 0)
»

http://pubs.opengroup.org/onlinepubs/9699919799/basedefs/assert.h.html

Am 31.07.2014 21:59, schrieb bearophile:
> Daniel Gibson:
>
>> so they can make sure to use assert() accordingly.
>
> What's the correct way to use the assert-assume hybrid?

I guess in many cases I'd avoid using assert() in fear of breaking my defensively written program (like that example from earlier: assert(x !is null); if(x) { x.foo = 42; }).

All this pretty much sounds like, if I should ever write any serious software in D in the future, I'd use assert() like assume() and I'd write my own dumbAssert() that does checks in debug mode and does nothing in release mode and is ignored by the optimizer (hopefully.. until it gets too smart again and starts evaluating debug code paths in hope of inferring something about the program state in release builds).

Actually, this somehow makes me afraid of D's design by contract stuff that will probably also be used by the optimizer in the same way..

Somehow all this assumes that you found all problems (at least the ones you check in assert()) by testing during development..
*I* personally wouldn't be so arrogant to assume that my code is bugfree just because it passed testing...

Cheers,
Daniel

On 7/31/2014 4:36 AM, bearophile wrote:
> (The problem is that your have defined your own idea,

"My" idea is the conventional one for assert - see the Wikipedia entry on it.

  -- http://en.wikipedia.org/wiki/Assertion_(software_development)

Yes, that article also says: "Under abnormal conditions, disabling assertion checking can mean that a program that would have aborted will continue to run. This is sometimes preferable." The last statement is in contradiction with the rest of the article, and I don't agree with it.


> so what I can show you
> will look meaningless or not comformant to your own definition. So this
> discussion is going nowhere. And my original topic drowns in this assume/assert
> debate that is off-topic.)
>
>
> In the case of assume:
>
>
> int max(in int x, in int y) {
>      assume(x > y);
>      return (x > y) ? x : y;
> }
>
> The optimizer is free to replace that code with this, even in debug builds:
>
> int max(in int x, in int y) {
>      return x;
> }

That implies that the behavior is undefined if the assumption is false. A compiler is free to add checks for undefined behavior (you yourself are a huge proponent of this) and people would (very reasonably for a quality implementation) expect that the assumption is checked. Hence, it will behave like assert.


> In the case of assert:
>
> int max(in int x, in int y) {
>      assert(x > y);
>      return (x > y) ? x : y;
> }
>
>
> In debug builds gets rewritten as:
>
> int max(in int x, in int y) {
>      if (x <= y)
>          throw new AssertError("...");
>      return x;
> }

Note how that behaves like assume.


> And in release builds gets rewritten as:
>
> int max(in int x, in int y) {
>      return (x > y) ? x : y;
> }

To require that the code be valid with x>y is to misunderstand what contract programming is all about. An assert is a contract and must be valid, whether it is checked or not. -release is not to be used to deliberately change the semantics of code.

For example, from the wikipedia article:

"Assertions are distinct from routine error-handling. Assertions document logically impossible situations and discover programming errors: if the impossible occurs, then something fundamental is clearly wrong. This is distinct from error handling: most error conditions are possible, although some may be extremely unlikely to occur in practice. Using assertions as a general-purpose error handling mechanism is unwise: assertions do not allow for recovery from errors; an assertion failure will normally halt the program's execution abruptly."

Note "LOGICALLY IMPOSSIBLE SITUATIONS", uppercased for emphasis. These are not my weird unique made-up-on-the-spot out-of-step ideas.

Code that relies on assertions being false is semantically broken.

In closing, Hoare's paper:

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

speaks of "assertions" which can be proven to be true. (It doesn't mention "assumptions".) The simplest way to prove it is to put in a runtime check. D's assert() nicely fits in with that.

On 7/31/2014 4:43 AM, bearophile wrote:
>> In debug builds gets rewritten as:
>>
>> int max(in int x, in int y) {
>>     if (x <= y)
>>         throw new AssertError("...");
>>     return x;
>> }
>
>
> Sorry, I meant:
>
> In debug builds gets rewritten as:
>
> int max(in int x, in int y) {
>      if (x <= y)
>          throw new AssertError("...");
>      return (x > y) ? x : y;
> }

You're overlooking data flow analysis, again. Please read up on it.

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.

> You're denying the existence of mathematical identities applied to symbolic math.

I am just going off of what you said and pointing out the consequences. You said it was a misuse to use asserts to verify inputs. So what is defined as an input?

int x = getIntFromSomeWhere(); // this is an input
int y = x; // Is y an input?
int z = x/2; // Is z an input?
real w = sin(x); // Is w an input?
int a = (x == 2)?1:0; // Is a an input?

> I suggest revisiting the notion of program logic correctness vs input verification.

The proposed optimizations to assert have brought into question the logical correctness of assert, that is what this whole thread is about(well not originally but that is what it is about now, sorry bearophile). Until that is resolved I am no longer going to use assert.