2qdxy4rzwzuui...@potatochowder.com writes: > On 2021-09-10 at 15:08:19 -0600, > Joe Pfeiffer <pfeif...@cs.nmsu.edu> wrote: > >> r...@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. -- https://mail.python.org/mailman/listinfo/python-list
