dicho.py 840 Bytes
 Jean-Christophe Filliâtre committed Jan 31, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 `````` from random import randint n = 42 a = [0] * n a[0] = randint(0, 100) i = 1 while i < n: #@ invariant 1 <= i #@ invariant forall i1, i2. 0 <= i1 <= i2 < i -> a[i1] <= a[i2] 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) v = input("quelle valeur cherchez-vous : ") l = 0 u = n-1 r = -1 `````` Jean-Christophe Filliâtre committed Jan 31, 2017 24 ``````while l <= u: `````` Jean-Christophe Filliâtre committed Jan 31, 2017 25 `````` #@ invariant 0 <= l and u < n `````` Jean-Christophe Filliâtre committed Jan 31, 2017 26 27 `````` #@ invariant r == -1 #@ invariant forall i. 0 <= i < n -> a[i] == v -> l <= i <= u `````` Jean-Christophe Filliâtre committed Jan 31, 2017 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 `````` #@ variant u-l m = (l + u) // 2 #@ assert l <= m and m <= u if a[m] < v: l = m+1 elif a[m] > v: u = m-1 else: #@ assert a[m] == v r = m break #@ assert -1 <= r < n #@ assert if r >= 0 then a[r] == v else forall i. 0 <= i < n -> a[i] != v ``````