[Issue 9300] Syntax for loop invariants

[d-bugmail at puremagic.com]

https://issues.dlang.org/show_bug.cgi?id=9300

Bolpat <qs.il.paperinik at gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |qs.il.paperinik at gmail.com

--- Comment #4 from Bolpat <qs.il.paperinik at gmail.com> ---
(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; }
```

--