haael writes:
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
Can you do this with a context manager? The syntax would be now_values = None while running_condition(...): with invariant_conditions(now_values, invariant1, ...): # loop body goes here The idea is that the __enter__ of the invariant_conditions context manager would initialize 'now_values' to [False] * invariants_count if now_values == None. The __exit__ would loop over zip(now_values, invariants), doing prev_value = now_value now_value = invariant(...) assert now_value if prev_value else True for each. An alternative definition of loop invariant from Wikipedia (https://en.wikipedia.org/wiki/Loop_invariant) suggest the simpler syntax (and implementation) while running_condition(...): with invariant_conditions(invariant1, ...): # loop body goes here where the invariants are simply asserted in __enter__, stored in an attribute of the context manager object, and asserted again in __exit__. In both cases, the evaluations would be controlled by a global variable, which would have minimal performance impact. You may also want to look at MacroPy, which allows you to implement syntax like you've proposed. Steve