| |
 | Posted by Bolpat |  Permalink Reply |
|
Bolpat 
| https://issues.dlang.org/show_bug.cgi?id=9300
Bolpat <qs.il.paperinik@gmail.com> changed:
What |Removed |Added
----------------------------------------------------------------------------
CC| |qs.il.paperinik@gmail.com
--- Comment #4 from Bolpat <qs.il.paperinik@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; }
```
--
|
