test.py 296 Bytes
Newer Older
1

2 3
a = 0
b = 1
4 5
l = range(0, 10)
## assert forall i. 0 <= i < 10 -> l[i] >= 0
6
while b < 100:
7 8 9
  ## invariant b >= a >= 0
  ## invariant b >= 1
  ## variant 200 - b - a
10 11
  print(a)
  b = a+b
12
  ## assert b >= 1
13
  a = b-a
14 15 16 17

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