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