test.py 234 Bytes
Newer Older
1

2 3 4
a = 0
b = 1
while b < 100:
5 6 7
  ## invariant b >= a >= 0
  ## invariant b >= 1
  ## variant 200 - b - a
8 9
  print(a)
  b = a+b
10
  ## assert b >= 1
11
  a = b-a
12 13 14 15

# Local Variables:
# compile-command: "make -C ../.. && why3 ide test.py"
# End: