test.py 689 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 27 28 29 30 31 32 33 34 35 36 ``````for x in l: print(x) # # arithmetic # # Python's division is not *Euclidean* division # q = -4 // 3 # #@ assert q == -2 # r = -4 % 3 # #@ assert r == 2 # #@ assert 4 // -3 == -2 # #@ assert 4 % -3 == -2 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 37 `````` `````` Jean-Christophe Filliâtre committed Jan 29, 2017 38 ``````# Local Variables: `````` Jean-Christophe Filliâtre committed Jan 30, 2017 39 ``````# compile-command: "make -C ../.. && why3 prove -P alt-ergo test.py" `````` Jean-Christophe Filliâtre committed Jan 29, 2017 40 ``# End:``