Friday Finking: Contorted loops
Joe Pfeiffer
pfeiffer at cs.nmsu.edu
Fri Sep 10 22:48:22 EDT 2021
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.
More information about the Python-list
mailing list