mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
42 lines
799 B
Python
42 lines
799 B
Python
|
|
from random import randint
|
|
|
|
n = 42
|
|
a = [0] * n
|
|
#@ assert len(a) == n
|
|
|
|
a[0] = randint(0, 100)
|
|
for i in range(1, n):
|
|
#@ 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)
|
|
v = int(input("quelle valeur cherchez-vous : "))
|
|
|
|
l = 0
|
|
u = n-1
|
|
r = -1
|
|
while l <= u:
|
|
#@ invariant 0 <= l and u < n
|
|
#@ invariant r == -1
|
|
#@ invariant forall i. 0 <= i < n -> a[i] == v -> l <= i <= u
|
|
#@ variant u-l
|
|
m = (l + u) // 2
|
|
if a[m] < v:
|
|
l = m+1
|
|
elif a[m] > v:
|
|
u = m-1
|
|
else:
|
|
r = m
|
|
break
|
|
|
|
if r == -1:
|
|
#@ assert forall i. 0 <= i < n -> a[i] != v
|
|
print("valeur absente")
|
|
else:
|
|
#@ assert a[r] == v
|
|
print("position", r)
|
|
|