tests/test.py

   1
   2 from random import randint
   3
   4 #@ lemma G: (1==1  so 2==2) and (2==2 by 1==1)
   5
   6 def f(x):
   7   #@ ensures result > x
   8   return x+1
   9
  10 def swap(a, i, j):
  11   #@ requires 0 <= i < len(a) and 0 <= j < len(a)
  12   t = a[i]
  13   a[i] = a[j]
  14   a[j] = t
  15
  16 def t10():
  17   s = 0
  18   for i in range(0, 11):
  19     #@ invariant 2 * s == i * (i-1)
  20     s = s + i
  21   #@ assert s == 55
  22
  23 i = randint(0, 10)
  24 #@ assert 0 <= i <= 10
  25
  26 a = 0
  27 b = 1
  28 while b < 100:
  29   #@ invariant b >= a >= 0
  30   #@ invariant b >= 1
  31   #@ variant 200 - b - a
  32   print(a)
  33   b = a+b
  34   #@ assert b >= 1
  35   a = b-a
  36
  37 # lists
  38 l = range(0, 10)
  39 #@ assert forall i. 0 <= i < 10 -> l[i] >= 0
  40 l[2] = 42
  41 #@ assert l[2] == 42
  42 i = 0
  43 while i < 10:
  44   #@ invariant 0 <= i
  45   #@ invariant forall j. 0 <= j < i -> l[j] == 0
  46   #@ variant 10 - i
  47   l[i] = 0
  48   i = i+1
  49
  50 sum = 0
  51 #@ label L
  52 for x in [42]*3:
  53   #@ invariant sum >= 0
  54   print(x)
  55   #@ assert x >= 0
  56   sum = sum+x
  57
  58 foo = [1,2,3]
  59 #@ assert len(foo)==3
  60 #@ assert foo[1]==2
  61
  62 #@ assert at(sum, L) == 0
  63
  64 #@ constant
  65 N = 42
  66
  67 #@ lemma L: N == 42
  68
  69 x, y = 1, 2
  70 #@ assert x == 1 and y == 2
  71 x, y = y, x
  72 #@ assert x == 2 and y == 1
  73
  74 #
  75 # Python's division is neither Euclidean division, nor computer division
  76 #@ assert  4 //  3 ==  1 and  4 %  3 ==  1
  77 #@ assert -4 //  3 == -2 and -4 %  3 ==  2
  78 #@ assert  4 // -3 == -2 and  4 % -3 == -2
  79 #@ assert -4 // -3 ==  1 and -4 % -3 == -1
  80
  81 #@ function
  82 def mfact(n) -> int:
  83     #@ variant n
  84     return 1 if n <= 0 else n*mfact(n-1)
  85
  86 n = len([0] + [1])
  87 #@ assert n == 2
  88
  89 # Local Variables:
  90 # compile-command: "make -C .. -j2 && why3 prove -P alt-ergo test.py"
  91 # End:
  92