## Binary search

Searching a sorted array for a given value, in logarithmic time.

Made famous by Bentley's Programming Pearls.

Authors: Jean-Christophe Filliâtre

Tools: Why3

References: The VerifyThis Benchmarks

see also the index (by topic, by tool, by reference, by year)

```(* 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
```

download ZIP archive