haael wrote: > 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
If something like this would be appropriate to have, then maybe it would be more appropriate to have a more generic-purpose DbC-like capability that could be used to check various kinds of pre/post conditions around various kinds of code construct. _______________________________________________ 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/TEBTN2W4TNZUCELN3ZBORZEYWSYI6XHK/ Code of Conduct: http://python.org/psf/codeofconduct/
