1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
/*@ axiom mean_1 : \forall int x, int y; x <= y => x <= (x+y)/2 <= y */
/*@ requires
@ n >= 0 && \valid_range(t,0,n-1) &&
@ \forall int k1, int k2; 0 <= k1 <= k2 <= n-1 => t[k1] <= t[k2]
@ ensures
@ (\result >= 0 && t[\result] == v) ||
@ (\result == -1 && \forall int k; 0 <= k < n => t[k] != v)
@*/
int binary_search(int* t, int n, int v) {
int l = 0, u = n-1, p = -1;
/*@ invariant
@ 0 <= l && u <= n-1 && -1 <= p <= n-1
@ && (p == -1 => \forall int k; 0 <= k < n => t[k] == v => l <= k <= u)
@ && (p >= 0 => t[p]==v)
@ variant u-l
@*/
while (l <= u ) {
int m = (l + u) / 2;
//@ assert l <= m <= u
if (t[m] < v)
l = m + 1;
else if (t[m] > v)
u = m - 1;
else {
p = m; break;
}
}
return p;
}
|
