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