www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 9300] New: Syntax for loop invariants

reply d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=9300

           Summary: Syntax for loop invariants
           Product: D
           Version: D2
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: enhancement
          Priority: P2
         Component: DMD
        AssignedTo: nobody puremagic.com
        ReportedBy: bearophile_hugs eml.cc



The two main missing parts of D contract programming are the "old" (pre-state)
and Loop Invariants. This enhancement request is about Loop Invariants.

A D Loop Invariant is just a just one or more asserts that must pass for a loop
inside a function to be considered correct.

In D it's possible to write loop invariants with regular asserts (if you want
in an inner scope, to group all the invariant asserts and to keep the loop
scope more clean:



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;

    {
        // This inner scope is the loop invariant.
        assert(y >= 1 && r >= 0);
        assert(y * (1 << r) <= x);
    }
    while (y > 1) {
        y /= 2;
        assert(r < x); // Regular assert.
        r++;
        {
            // This inner scope is the loop invariant.
            assert(y >= 1 && r >= 0);
            assert(y * (1 << r) <= x);
        }
    }

    return r;
} unittest {
    assert(iLog2(1) == 0);
    assert(iLog2(2) == 1);
    assert(iLog2(3) == 1);
    assert(iLog2(4) == 2);
    foreach (immutable k; 1 .. 31) {
        assert(iLog2(1 << k) == k);
        assert(iLog2((1 << k) - 1) == k - 1);
        assert(iLog2((1 << k) + 1) == k);
    }
}

void main() {}



But I suggest to allow a invariant(){} block in for/foreach/while/do-while
loops. A possible syntax:


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;
}


An alternative syntax:

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);
        }
        y /= 2;
        assert(r < x); // Regular assert.
        r++;
    }

    return r;
}


Another possible syntax:


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) {
        y /= 2;
        assert(r < x); // Regular assert.
        r++;
    } invariant() {
        assert(y >= 1 && r >= 0);
        assert(y * (1 << r) <= x);
    }

    return r;
}



invariant(){} has some advantages:
- Just like in{} and out(){} it gives the programmer a visual aid, to recognize
that part of the code as actually the loop invariant.
- Having a simple loop invariant syntax built in the language encourages and
reminds programmers to use them.
- Even if not every D programmer uses them, programmers that want to write more
reliable code, or library code, are free to use loop invariants. It's important
to reason about loop invariants. They are taught in most computer science
courses.
- Maybe it makes life easer to static analysis tools for D code.


A loop invariant must be true every time just before the exit condition is
tested. This has some consequences:
- A programmer is allowed to add one invariant(){} to a loop. This invariant
will always run in the right moment. On the other hand if a programmer uses
just asserts, they need to be copied before the loop entry, as in the example
I've shown.
- If you want to write a loop invariant, but you don't use invariant(){} and
the loop contains one or more "continue", things gets complex. This is similar
to out(){}, that is guaranteed to run at the function end (if there are no
exceptions or errors) even in presence of multiple return statements. This is
important.

More notes:
- I think the implementation of this feature is easy.
- There are also "loop variants", but they are less common, and they are not
discussed in this enhancement request.
- It's a backward compatible change, it doesn't break any old D code.
- The meaning of invariant(){} inside loops is easy to understand, it's not a
cryptic feature; and the "invariant" keyword is already present and used to
struct/class invariants, that is a similar purpose.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
Jan 12 2013
next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=9300




Loop invariants were part of the D spec, a long time ago. They were discarded
as being of negligible value.

Compared to an assert, plus a comment, what do they add?

   while (cond) 
   {
       // Loop invariant
       assert( xxx );
       ...
   }

Definitely the concept is very useful for reasoning about code. But that
doesn't mean it needs specific language syntax. For example, it's easy for a
static analysis tool to recognize this as a loop invariant. And I don't think
you'll find a syntax that is nicer than what I wrote above!

This is a feature which was previously evaluated and rejected.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
Feb 05 2013
prev sibling next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=9300






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: -------
Feb 05 2013
prev sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=9300







 All D books and tutorials will have a chapter about loop invariants,


Well, one or few paragraphs :-)

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