python: better annotations for dicho.py

parent 04715397
......@@ -9,6 +9,7 @@ i = 1
while i < n:
#@ invariant 1 <= i
#@ 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
......@@ -25,23 +26,20 @@ 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
#@ 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
if r == -1:
#@ assert forall i. 0 <= i < n -> a[i] != v
print("valeur absente")
else:
#@ assert a[r] == v
print("position", r)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment