Welcome, guest | Sign In | My Account | Store | Cart

Eiffel like loop variant assertion

Python, 27 lines
 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.

1 comment

Alain Pointdexter 20 years, 10 months ago  # | flag

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!