[Issue 9300] Syntax for loop invariants

[d-bugmail at puremagic.com]

http://d.puremagic.com/issues/show_bug.cgi?id=9300



--- Comment #2 from bearophile_hugs at eml.cc 2013-02-05 04:21:47 PST ---
(In reply to comment #1)

Thank you for your answers.

> Loop invariants were part of the D spec, a long time ago.

I didn't know this.


> Compared to an assert, plus a comment, what do they add?
> 
>    while (cond) 
>    {
>        // Loop invariant
>        assert( xxx );
>        ...
>    }

Now think about adding some more parts to that while loop, with one or more
"continue". Now where do you put that assert? You have to duplicate your
assert:

   while (cond) 
   {
       if (predicate()) {
           assert( xxx ); // Loop invariant
           continue;
       }
       ... // some code here
       assert( xxx ); // Loop invariant
       ...
   }

If instead of an assert you have more code (maybe inside a scope {}) your code
gets redundant.

A invariant{} piece of code is guaranteed by the compiler to be run in the
right moment of the loop, just like out(){} is guaranteed to be run after every
return contained in a function. This frees the programmer from the need to
think where to put the loop invariant.


> For example, it's easy for a
> static analysis tool to recognize this as a loop invariant.

Take a look here, this loop has both loop invariant code and a free assert(r <
x) that's not part of the invariant. Is your static analysis tool so able to
tell them apart?


int iLog2(in int x) pure nothrow @safe
in {
    assert(x >= 1);
} out(result) {
    assert(result >= 0);
    assert((1 << result) <= x);
} body {
    int r = 0;
    int y = x;

    while (y > 1) 
        invariant() {
            assert(y >= 1 && r >= 0);
            assert(y * (1 << r) <= x);
        } body {
            y /= 2;
            assert(r < x); // Regular assert.
            r++;
        }

    return r;
}


> And I don't think you'll find a syntax that is nicer
> than what I wrote above!

Your example is too much simple and short.
And generally it's good to have ways to communicate semantics to the compiler,
instead of using a comment.

And it's not just a matter of compilers: having a built-in syntax encourages
people to take it in account. I have met people that didn't know about contract
programming before seeing the D syntax for contracts. Sometimes having a syntax
is a way to teach something to programmers.

A programmer is supposed to know what a loop invariant (and variant) is, but if
you offer them a syntax staple I think they will be a bit more willing to think
about loop invariants. A syntax gives a frame for the mind to think about that.
All D books and tutorials will have a chapter about loop invariants, this will
raise the awareness about those invariants. Even if only high-grade D programs
will have loop invariants, it will be an improvement.

I think the amount of new syntax required by this enhancement request is quite
small.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------