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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
module MaxArray
use int.Int
use array.Array
let cfg compute_max (a:array int) : (max: int, ghost ind:int)
requires { length a > 0 }
ensures { 0 <= ind < length a }
ensures { forall i. 0 <= i < length a -> a[ind] >= a[i] }
=
(* simulation of the C code: (from ACSL Manual, section 2.4.2 Loop invariants)
i = 0;
goto L;
do {
if (t[i] > m) { L: m = t[i]; }
/*@ invariant
@ 0 <= i < n && m == \max(0,i,\lambda integer k; t[k]);
@*/
i++;
}
while (i < n);
return m;
*)
var i m: int;
ghost var ind: int;
{
i <- 0;
goto L
}
L {
m <- a[i];
ind <- i;
goto L1
}
L1 {
invariant i_bounds { 0 <= i < length a };
invariant ind_bounds { 0 <= ind < length a };
invariant m_and_ind { m = a[ind] };
invariant m_is_max { forall j. 0 <= j <= i -> m >= a[j] };
(* (yes, j <= i, not j < i !) *)
i <- i + 1;
switch (i < length a)
| True -> goto L2
| False -> return (m, ind)
end
}
L2 {
switch (a[i] > m)
| True -> goto L
| False -> goto L1
end
}
end
|
