Friday Finking: Contorted loops

[Joe Pfeiffer]

2QdxY4RzWzUUiLuE at potatochowder.com writes:

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

Precisely because you've got knowledge of the exit condition on
iterations after the first, but not the first one.  So, unlike a while
loop, you don't have the same knowledge on every pass.

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