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
|
(*
We look for the first occurrence of zero in an array of integers.
The values have the following property: they never decrease by more than one.
The code makes use of that property to speed up the search.
*)
module Decrease1
use int.Int
use ref.Ref
use array.Array
predicate decrease1 (a: array int) =
forall i: int. 0 <= i < length a - 1 -> a[i+1] >= a[i] - 1
let rec lemma decrease1_induction (a: array int) (i j: int) : unit
requires { decrease1 a }
requires { 0 <= i <= j < length a }
ensures { a[j] >= a[i] + i - j }
variant { j - i }
= if i < j then decrease1_induction a (i+1) j
let search (a: array int)
requires { decrease1 a }
ensures {
(result = -1 /\ forall j: int. 0 <= j < length a -> a[j] <> 0)
\/ (0 <= result < length a /\ a[result] = 0 /\
forall j: int. 0 <= j < result -> a[j] <> 0) }
= let i = ref 0 in
while !i < length a do
invariant { 0 <= !i }
invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 }
variant { length a - !i }
if a[!i] = 0 then return !i;
if a[!i] > 0 then i := !i + a[!i] else i := !i + 1
done;
-1
let rec search_rec (a: array int) (i : int)
requires { decrease1 a /\ 0 <= i }
ensures {
(result = -1 /\ forall j: int. i <= j < length a -> a[j] <> 0)
\/ (i <= result < length a /\ a[result] = 0 /\
forall j: int. i <= j < result -> a[j] <> 0) }
variant { length a - i }
= if i < length a then
if a[i] = 0 then i
else if a[i] > 0 then search_rec a (i + a[i])
else search_rec a (i + 1)
else
-1
end
|
