3 A classical example. Searches a sorted array for a given value v. *)
8 use int.ComputerDivision
12 (* the code and its specification *)
14 exception Not_found (* raised to signal a search failure *)
16 let binary_search (a : array int) (v : int) : int
17 requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
18 ensures { 0 <= result < length a /\ a[result] = v }
19 raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
22 let u = ref (length a - 1) in
24 invariant { 0 <= !l /\ !u < length a }
26 forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
28 let m = !l + div (!u - !l) 2 in
29 assert { !l <= m <= !u };
41 (* A generalization: the midpoint is computed by some abstract function.
42 The only requirement is that it lies between l and u. *)
44 module BinarySearchAnyMidPoint
50 exception Not_found (* raised to signal a search failure *)
52 val midpoint (l:int) (u:int) : int
53 requires { l <= u } ensures { l <= result <= u }
55 let binary_search (a :array int) (v : int) : int
56 requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
57 ensures { 0 <= result < length a /\ a[result] = v }
58 raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
61 let u = ref (length a - 1) in
63 invariant { 0 <= !l /\ !u < length a }
65 forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
67 let m = midpoint !l !u in
79 (* binary search using 32-bit integers *)
81 module BinarySearchInt32
86 use mach.array.Array32
88 (* the code and its specification *)
90 exception Not_found (* raised to signal a search failure *)
92 let binary_search (a : array int32) (v : int32) : int32
93 requires { forall i1 i2 : int. 0 <= i1 <= i2 < a.length ->
95 ensures { 0 <= result < a.length /\ a[result] = v }
97 forall i:int. 0 <= i < a.length -> a[i] <> v }
100 let u = ref (length a - 1) in
102 invariant { 0 <= !l /\ !u < a.length }
103 invariant { forall i : int. 0 <= i < a.length ->
104 a[i] = v -> !l <= i <= !u }
106 let m = !l + (!u - !l) / 2 in
107 assert { !l <= m <= !u };
110 else if a[m] > v then
119 (* A particular case with Boolean values (0 or 1) and a sentinel 1 at the end.
120 We look for the first position containing a 1. *)
122 module BinarySearchBoolean
125 use int.ComputerDivision
129 let binary_search (a: array int) : int
130 requires { 0 < a.length }
131 requires { forall i j. 0 <= i <= j < a.length -> 0 <= a[i] <= a[j] <= 1 }
132 requires { a[a.length - 1] = 1 }
133 ensures { 0 <= result < a.length }
134 ensures { a[result] = 1 }
135 ensures { forall i. 0 <= i < result -> a[i] = 0 }
138 let hi = ref (length a - 1) in
140 invariant { 0 <= !lo <= !hi < a.length }
141 invariant { a[!hi] = 1 }
142 invariant { forall i. 0 <= i < !lo -> a[i] = 0 }
143 variant { !hi - !lo }
144 let mid = !lo + div (!hi - !lo) 2 in