On 11/04/20 5:38 pm, Steven D'Aprano wrote:
That is surely okay though. If the loop is never entered at all, by the principle of vacuous truth the condition inside the loop is true.
No. A loop invariant is something that is true before entering the loop, and remains true after each iteration. This is so that you can assert (loop_invariant and termination_condition) after the loop finishes, even if it executes zero times.
One of the reasons people sometimes suggest adding new syntax for asserting loop invariants is that it's currently awkward to do all of this properly without writing the invariant twice.