[Issue 9300] New: Syntax for loop invariants

[d-bugmail at puremagic.com]

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 at puremagic.com
        ReportedBy: bearophile_hugs at eml.cc


--- Comment #0 from bearophile_hugs at eml.cc 2013-01-12 03:46:17 PST ---
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: -------