(* Binary search A classical example. Searches a sorted array for a given value v. *) module BinarySearch use int.Int use int.ComputerDivision use ref.Ref use array.Array (* the code and its specification *) exception Not_found (* raised to signal a search failure *) let binary_search (a : array int) (v : int) : int requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] } ensures { 0 <= result < length a /\ a[result] = v } raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v } = let l = ref 0 in let u = ref (length a - 1) in while !l <= !u do invariant { 0 <= !l /\ !u < length a } invariant { forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } variant { !u - !l } let m = !l + div (!u - !l) 2 in assert { !l <= m <= !u }; if a[m] < v then l := m + 1 else if a[m] > v then u := m - 1 else return m done; raise Not_found end (* A generalization: the midpoint is computed by some abstract function. The only requirement is that it lies between l and u. *) module BinarySearchAnyMidPoint use int.Int use ref.Ref use array.Array exception Not_found (* raised to signal a search failure *) val midpoint (l:int) (u:int) : int requires { l <= u } ensures { l <= result <= u } let binary_search (a :array int) (v : int) : int requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] } ensures { 0 <= result < length a /\ a[result] = v } raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v } = let l = ref 0 in let u = ref (length a - 1) in while !l <= !u do invariant { 0 <= !l /\ !u < length a } invariant { forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u } variant { !u - !l } let m = midpoint !l !u in if a[m] < v then l := m + 1 else if a[m] > v then u := m - 1 else return m done; raise Not_found end (* The following version of binary search is faster in practice, by being friendlier with the branch predictor of most processors. It also happens to be stable, since it always return the highest index. *) module BinarySearchBranchless use int.Int use int.ComputerDivision use ref.Ref use array.Array exception Not_found (* raised to signal a search failure *) let binary_search (a : array int) (v : int) : int requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] } ensures { 0 <= result < length a /\ a[result] = v } ensures { forall i : int. result < i < length a -> a[i] <> v } raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v } = let l = ref 0 in let s = ref (length a) in if !s = 0 then raise Not_found; while !s > 1 do invariant { 0 <= !l /\ !l + !s <= length a /\ !s >= 1 } invariant { forall i : int. 0 <= i < length a -> a[i] = v -> a[!l] <= v /\ i < !l + !s } variant { !s } let h = div !s 2 in let m = !l + h in l := if a[m] > v then !l else m; s := !s - h; done; if a[!l] = v then !l else raise Not_found end (* binary search using 32-bit integers *) module BinarySearchInt32 use int.Int use mach.int.Int32 use ref.Ref use mach.array.Array32 exception Not_found (* raised to signal a search failure *) let binary_search (a : array int32) (v : int32) : int32 requires { forall i1 i2 : int. 0 <= i1 <= i2 < a.length -> a[i1] <= a[i2] } ensures { 0 <= result < a.length /\ a[result] = v } raises { Not_found -> forall i:int. 0 <= i < a.length -> a[i] <> v } = let l = ref 0 in let u = ref (length a - 1) in while !l <= !u do invariant { 0 <= !l /\ !u < a.length } invariant { forall i : int. 0 <= i < a.length -> a[i] = v -> !l <= i <= !u } variant { !u - !l } let m = !l + (!u - !l) / 2 in assert { !l <= m <= !u }; if a[m] < v then l := m + 1 else if a[m] > v then u := m - 1 else return m done; raise Not_found end (* A particular case with Boolean values (0 or 1) and a sentinel 1 at the end. We look for the first position containing a 1. *) module BinarySearchBoolean use int.Int use int.ComputerDivision use ref.Ref use array.Array let binary_search (a: array int) : int requires { 0 < a.length } requires { forall i j. 0 <= i <= j < a.length -> 0 <= a[i] <= a[j] <= 1 } requires { a[a.length - 1] = 1 } ensures { 0 <= result < a.length } ensures { a[result] = 1 } ensures { forall i. 0 <= i < result -> a[i] = 0 } = let lo = ref 0 in let hi = ref (length a - 1) in while !lo < !hi do invariant { 0 <= !lo <= !hi < a.length } invariant { a[!hi] = 1 } invariant { forall i. 0 <= i < !lo -> a[i] = 0 } variant { !hi - !lo } let mid = !lo + div (!hi - !lo) 2 in if a[mid] = 1 then hi := mid else lo := mid + 1 done; !lo end