Binary Search (Seq)
Binary search in a sorted (mathematical) sequence
/* Binary search in a sorted sequence */
method binary_search(xs: Seq[Int], key: Int) returns (index: Int)
requires forall i: Int, j: Int :: 0 <= i && j < |xs| && i < j ==> xs[i] < xs[j]
ensures -1 <= index && index < |xs|
ensures 0 <= index ==> xs[index] == key
ensures -1 == index ==> (forall i: Int :: 0 <= i && i < |xs| ==> xs[i] != key)
{
var low: Int := 0
var high: Int := |xs|
index := -1
while (low < high && index == -1)
invariant 0 <= low && low <= high && high <= |xs|
invariant index == -1 ==> forall i: Int :: (0 <= i && i < |xs| && !(low <= i && i < high)) ==> xs[i] != key
invariant -1 <= index && index < |xs|
invariant 0 <= index ==> xs[index] == key
{
var mid: Int := (low + high) \ 2
if (xs[mid] < key) {
low := mid + 1
} else {
if (key < xs[mid]) {
high := mid
} else {
index := mid
high := mid
}
}
}
}