The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata

## 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

```(* Binary search

A classical example. Searches a sorted array for a given value v. *)

module BinarySearch

use import int.Int
use import int.ComputerDivision
use import ref.Ref
use import array.Array

(* the code and its specification *)

exception Break int (* raised to exit the loop *)
exception Not_found (* raised to signal a search failure *)

let binary_search (a :array int) (v : 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 }
= try
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
raise (Break m)
done;
raise Not_found
with Break i ->
i
end

end

(* A generalization: the midpoint is computed by some abstract function.
The only requirement is that is lies between l and u. *)

module BinarySearchAnyMidPoint

use import int.Int
use import ref.Ref
use import array.Array

exception Break int (* raised to exit the loop *)
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)
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 }
= try
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
raise (Break m)
done;
raise Not_found
with Break i ->
i
end

end

(* binary search using 32-bit integers *)

module BinarySearchInt32

use import arith.Int32
use import ref.Ref
use import array.Array

(* the code and its specification *)

exception Break int (* raised to exit the loop *)
exception Not_found (* raised to signal a search failure *)

let binary_search (a :array int) (v : int)
requires { 0 <= length a <= max_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 }
= try
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
raise (Break m)
done;
raise Not_found
with Break i ->
i
end

end
```