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