Friday Finking: Contorted loops

[2QdxY4RzWzUUiLuE at potatochowder.com]

On 2021-09-10 at 15:08:19 -0600,
Joe Pfeiffer <pfeiffer at cs.nmsu.edu> wrote:

> ram at zedat.fu-berlin.de (Stefan Ram) writes:

> >   The existence of statements like "break" renders 
> >   proof techniques for loops (such as Hoare's) with
> >   their invariants and inference rules unapplicable.
> 
> Also the reason to avoid repeat-until loops:  the loop "invariant" isn't
> the same on the first iteration as on subsequent iterations.

I am by no means an expert, nor likely even a neophyte, but why would
the loop invariant not be the same on the first iteration?

I can certainly see that the exit condition may not make sense at the
beginning of the first iteration (e.g., there is not yet any data to
compare to the sentinel), but ISTM that claiming that the exit condition
is a loop invariant isn't kosher (because all you're claiming is that
the compiler works).

I can also see that certain state information may not be captured until
the end of the first iteration.  But presumably said state information
can change from iteration to iteration, so I can't see how you'd derive
an invariant involving it.