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.
haael
_______________________________________________
Python-ideas mailing list -- python-ideas@python.org
To unsubscribe send an email to python-ideas-le...@python.org
https://mail.python.org/mailman3/lists/python-ideas.python.org/
Message archived at
https://mail.python.org/archives/list/python-ideas@python.org/message/45242MS4OZ7EYFL5IE45GTLLPDRTPT7G/
Code of Conduct: http://python.org/psf/codeofconduct/
