Loop invariants

[monkyyy]

On Friday, 27 September 2024 at 18:10:13 UTC, Quirin Schroll 
wrote:
> 
> ```d
> int x = 10;
> assert(x >= 0);
> while (x > 0)
> {
>     assert(x >= 0);
>     scope(success) assert(x >= 0);
>     // loop body
> }
> assert(x >= 0); // not needed if the loop condition is ```

While not just simply make this to an (even worse) do-while loop

```d
int x=10;
do_allot{
   assert(x>=0);
} while(x>0){
   ...
}
```

where do_allot will run all these extra times?

> If you open a textbook or the Wikipedia page on Loop invariant, 
> it’ll tell you: A loop invariant must hold before the loop 
> runs, at the beginning of the loop, at the end of the loop, and 
> after the loop.

Why would wikipedias definition matter? If the current naive 
syntax of `foreach(...){assert()` runs N times, how much value is 
there in a special case that runs N+2 times?