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.
Eiffel Contracts in Python. Hi Sebastien, This is not a comment but a pointer to a comment i made to your great recipe for Design by Contracts. I make it here because the odds are greater that you consult this page rather than the other one and i am quite in a hurry. The problem is that your recipe doesn't seem to work on overridden inherited method. Keep the good work!