Bug 9300 – Syntax for loop invariants

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.

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.

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

(In reply to comment #2) > All D books and tutorials will have a chapter about loop invariants, Well, one or few paragraphs :-)

(In reply to Don from comment #1) > Compared to an assert, plus a comment, what do they add? A loop invariant must be true entering the loop and exiting the loop, including the case when the loop runs zero times. In 2024, the ideal syntax is an invariant block, syntactically identical to `invariant` blocks in aggregates, but actually more similar to function contracts: ```d while (cond) invariant(inv) { ... } ``` Which could lower to: ```d assert(inv); while (cond) { scope(success) assert(inv); ... } ``` The advantage is alleviating a DRY violation plus documenting intent. Also, getting it right isn’t trivial, actually. It took me a while to realize `scope(success)` would be needed and just putting it at the end of the loop simply isn’t enough. The lowering above assumes that the condition doesn’t have side-effects. For a `for` loop, it’s not entirely clear when exactly the invariant would be checked. Before or after the init? If before, nothing of the init part could be used as part of the invariant, which makes little sense. If after, expressing it boils down to: ```d for (Init; Cond; Inc) invariant (Inv) Body; // lowers to: for ({ Init; assert(Inv); } Cond; Inc) { scope(success) assert(Inv); Body; } ``` For completeness: ```d do invariant (Inv) Body; while (Cond); // lowers to: assert(Inv); do { scope(success) assert(Inv); Body; } while (Cond); ``` and ```d foreach (Var; Agg) invariant (Inv) Body; // lowers to assert(Inv); foreach (Var; Agg) { scope(success) assert(Inv); Body; } ```

It’s not entirely clear if an invariant should be checked if the loop is entered or left via `goto`. My sense is entering should not check the invariant, but exiting, I truly don’t know. `scope(success)` would check it.

THIS ISSUE HAS BEEN MOVED TO GITHUB https://github.com/dlang/dmd/issues/18512 DO NOT COMMENT HERE ANYMORE, NOBODY WILL SEE IT, THIS ISSUE HAS BEEN MOVED TO GITHUB