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