test.py 1.04 KB
Newer Older
1

2 3 4 5 6
from random import randint

i = randint(0, 10)
#@ assert 0 <= i <= 10

7 8 9 10 11 12
# def swap(a, i, j):
#   #@ requires 0 <= i < len(a) and 0 <= j < len(a)
#   t = a[i]
#   a[i] = a[j]
#   a[j] = t

13 14 15
a = 0
b = 1
while b < 100:
16 17 18
  #@ invariant b >= a >= 0
  #@ invariant b >= 1
  #@ variant 200 - b - a
19 20
  print(a)
  b = a+b
21
  #@ assert b >= 1
22
  a = b-a
23 24

# lists
25
l = range(0, 10)
26
#@ assert forall i. 0 <= i < 10 -> l[i] >= 0
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
27
l[2] = 42
28
#@ assert l[2] == 42
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
29 30
i = 0
while i < 10:
31 32 33
  #@ invariant 0 <= i
  #@ invariant forall j. 0 <= j < i -> l[j] == 0
  #@ variant 10 - i
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
34 35
  l[i] = 0
  i = i+1
36

37
sum = 0
38
for x in [42]*3:
39
  #@ invariant sum >= 0
40
  print(x)
41 42
  #@ assert x >= 0
  sum = sum+x
43

44 45 46 47 48
foo = [1,2,3]
#@ assert len(foo)==3
#@ assert foo[1]==2


49 50 51 52 53
# Python's division is neither Euclidean division, nor computer division
#@ assert  4 //  3 ==  1 and  4 %  3 ==  1
#@ assert -4 //  3 == -2 and -4 %  3 ==  2
#@ assert  4 // -3 == -2 and  4 % -3 == -2
#@ assert -4 // -3 ==  1 and -4 % -3 == -1
54

55
# Local Variables:
56
# compile-command: "make -C ../.. && why3 prove -P alt-ergo test.py"
57
# End:
58