Python has more and more optional tools for formal correctness cheking. Why not loop invariants?
Loop invariant is such a statement that if it was true before the loop iteration, it will also be true after the iteration. It can be implemented as an assertion of an implication.
now_value = False while running_condition(...): prev_value = now_value now_value = invariant_condition(...) assert now_value if prev_value else True
Here for ellipsis we can substitute any values and variables.
I propose the new syntax:
while running_condition(...): invariant invariant_condition(...)
The keyword 'invariant' is allowed only inside a loop. The interpreter will create a separate boolean variable holding the truth value of each invariant. On the loop entry, the value is reset to false. When the 'invariant' statement is encountered, the interpreter will evaluate the expression, test the implication 'prev_value -> now_value' and update the value. If the implication is not met, an exception will be thrown 'InvariantError' which is a subclass of 'AssertionError'.
Like assertions, invariants will be checked only in debug mode.
I am developing a library for formal proofs and such a feature would be handy.