test.py 1.04 KB
 Jean-Christophe Filliâtre committed Jan 29, 2017 1 `````` `````` Jean-Christophe Filliâtre committed Jan 30, 2017 2 3 4 5 6 ``````from random import randint i = randint(0, 10) #@ assert 0 <= i <= 10 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 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 `````` Jean-Christophe Filliâtre committed Jan 29, 2017 13 14 15 ``````a = 0 b = 1 while b < 100: `````` Jean-Christophe Filliâtre committed Jan 30, 2017 16 17 18 `````` #@ invariant b >= a >= 0 #@ invariant b >= 1 #@ variant 200 - b - a `````` Jean-Christophe Filliâtre committed Jan 29, 2017 19 20 `````` print(a) b = a+b `````` Jean-Christophe Filliâtre committed Jan 30, 2017 21 `````` #@ assert b >= 1 `````` Jean-Christophe Filliâtre committed Jan 29, 2017 22 `````` a = b-a `````` Jean-Christophe Filliâtre committed Jan 30, 2017 23 24 `````` # lists `````` Jean-Christophe Filliâtre committed Jan 30, 2017 25 ``````l = range(0, 10) `````` Jean-Christophe Filliâtre committed Jan 30, 2017 26 ``````#@ assert forall i. 0 <= i < 10 -> l[i] >= 0 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 27 ``````l[2] = 42 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 28 ``````#@ assert l[2] == 42 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 29 30 ``````i = 0 while i < 10: `````` Jean-Christophe Filliâtre committed Jan 30, 2017 31 32 33 `````` #@ invariant 0 <= i #@ invariant forall j. 0 <= j < i -> l[j] == 0 #@ variant 10 - i `````` Jean-Christophe Filliâtre committed Jan 30, 2017 34 35 `````` l[i] = 0 i = i+1 `````` Jean-Christophe Filliâtre committed Jan 29, 2017 36 `````` `````` Jean-Christophe Filliâtre committed Jan 30, 2017 37 ``````sum = 0 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 38 ``````for x in [42]*3: `````` Jean-Christophe Filliâtre committed Jan 30, 2017 39 `````` #@ invariant sum >= 0 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 40 `````` print(x) `````` Jean-Christophe Filliâtre committed Jan 30, 2017 41 42 `````` #@ assert x >= 0 sum = sum+x `````` Jean-Christophe Filliâtre committed Jan 30, 2017 43 `````` `````` Jean-Christophe Filliâtre committed Jan 30, 2017 44 45 46 47 48 ``````foo = [1,2,3] #@ assert len(foo)==3 #@ assert foo[1]==2 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 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 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 54 `````` `````` Jean-Christophe Filliâtre committed Jan 29, 2017 55 ``````# Local Variables: `````` Jean-Christophe Filliâtre committed Jan 30, 2017 56 ``````# compile-command: "make -C ../.. && why3 prove -P alt-ergo test.py" `````` Jean-Christophe Filliâtre committed Jan 29, 2017 57 ``````# End: `````` Jean-Christophe Filliâtre committed Jan 30, 2017 58