Eiffel like loop variant assertion
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
import sys def variant(expr): expr = int(expr) f = sys._getframe(1) name = "variant$%d"%f.f_lasti caller = f.f_locals try: result = (0<=expr<caller[name]) except KeyError: result = True caller[name] = expr return result # # sample # def test(): assert variant(1) # Not an error: only executed once per function call assert variant(1) # Not an error: this is another statement for x in range(100): assert variant(100-x) #Not an error: (100-x) decrease between loops #assert variant(1) #An error: 1 is constant for i in range(10): test()
The loop variant can be used to ensure that a loop will terminate after a finite number of iterations. It must be an integer expression whose value will be decreased by at least one, while remain non-negative, by any execution of the loop body; since a non-negative integer cannot be decreased forever, this ensures termination. The variant method is intended to be used in an assert statement, this allow to turn off checks with the -O flags. The assert statement will raise an exception if the variant is negative or does not decrease.
Ok the implementation is quite a hack ;-) The secret is to use the caller namespace, this make possible to store data between function calls.
It use the "variant$xxx" key to store data. Since $ can't be used in name identifiers it's impossible to get clashes with variable names. xxx is replaced by the caller opcode index; this make possible to have several variant() call in the same function.