test.py 639 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

# lists
14 15
l = range(0, 10)
## assert forall i. 0 <= i < 10 -> l[i] >= 0
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
16 17 18 19 20 21 22 23 24
l[2] = 42
## assert l[2] == 42
i = 0
while i < 10:
  ## invariant 0 <= i
  ## invariant forall j. 0 <= j < i -> l[j] == 0
  ## invariant len(l) == 10
  l[i] = 0
  i = i+1
25

26 27 28 29 30 31 32 33 34
# arithmetic
# Python's division is *Euclidean* division
q = -4 // 3
## assert q == -2
r = -4 % 3
## assert r == 2
## assert 4 // -3 == -2
## assert 4 % -3 == -2

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