test.py 639 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 29, 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 29, 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 15 ``````l = range(0, 10) ## assert forall i. 0 <= i < 10 -> l[i] >= 0 `````` Jean-Christophe Filliâtre committed Jan 30, 2017 16 17 18 19 20 21 22 23 24 ``````l[2] = 42 ## assert l[2] == 42 i = 0 while i < 10: ## invariant 0 <= i ## invariant forall j. 0 <= j < i -> l[j] == 0 ## invariant len(l) == 10 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 ``````# arithmetic # Python's division is *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 29, 2017 35 36 37 ``````# Local Variables: # compile-command: "make -C ../.. && why3 ide test.py" # End:``````