dicho.py 799 Bytes
Newer Older
1 2 3 4 5

from random import randint

n = 42
a = [0] * n
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
6
#@ assert len(a) == n
7 8

a[0] = randint(0, 100)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
9
for i in range(1, n):
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)
16
v = int(input("quelle valeur cherchez-vous : "))
17 18 19 20

l = 0
u = n-1
r = -1
21
while l <= u:
22
    #@ invariant 0 <= l and u < n
23 24
    #@ invariant r == -1
    #@ invariant forall i. 0 <= i < n -> a[i] == v -> l <= i <= u
25
    #@ variant   u-l
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

35
if r == -1:
36
    #@ assert forall i. 0 <= i < n -> a[i] != v
37 38
    print("valeur absente")
else:
39
    #@ assert a[r] == v
40 41
    print("position", r)