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