(* 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 } = [@vc:sp] 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 } = [@vc:sp] 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 (* binary search using 32-bit integers *) module BinarySearchInt32 use int.Int use mach.int.Int32 use ref.Ref use mach.array.Array32 (* the code and its specification *) 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 } = [@vc:sp] 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 } = [@vc:sp] 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