Commit 158b262b by Jean-Christophe Filliatre

tests Python

parent f6bdbefe
 ... ... @@ -3,17 +3,13 @@ from random import randint n = 42 a = [0] * n #@ assert len(a) == n a[0] = randint(0, 100) i = 1 while i < n: #@ invariant 1 <= i for i in range(1, n): #@ invariant forall i1, i2. 0 <= i1 <= i2 < i -> a[i1] <= a[i2] #@ variant n-i a[i] = a[i-1] + randint(0, 10) i = i + 1 #@ assert len(a) == n #@ assert forall i1, i2. 0 <= i1 <= i2 < len(a) -> a[i1] <= a[i2] print(a) ... ...
 ... ... @@ -15,12 +15,14 @@ if q < 0: r = 0 while q > 0: #@ invariant 0 <= q and r + p * q == a * b #@ invariant 0 <= q #@ invariant r + p * q == a * b #@ variant q print(p, q, r) if q % 2 == 1: r = r + p p = p + p q = q // 2 print(p, q, r) print("a * b =", r) #@ assert r == a * b
 ... ... @@ -7,8 +7,9 @@ n = int(input("entrez n : ")) s = 0 k = 0 while k <= n: #@ invariant 0 <= k <= n+1 #@ invariant k <= n+1 #@ invariant s == (k - 1) * k // 2 #@ variant n-k s = s + k k = k + 1 ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!