Binary Search (Quantified Permissions)
Binary search in a sorted (mutable) array
/* Binary search in a sorted array */
define access(a) forall j: Int :: 0 <= j && j < len(a) ==> acc(loc(a, j).val)
define untouched(a) forall j: Int :: 0 <= j && j < len(a) ==> loc(a, j).val == old(loc(a, j).val)
method binary_search(a: IArray, key: Int) returns (index: Int)
requires access(a)
requires forall i: Int, j: Int :: {loc(a, i), loc(a, j)} 0 <= i && j < len(a) && i < j ==> loc(a, i).val < loc(a, j).val
ensures access(a) && untouched(a)
ensures -1 <= index && index < len(a)
ensures 0 <= index ==> loc(a, index).val == key
ensures -1 == index ==> (forall i: Int :: 0 <= i && i < len(a) ==> loc(a,i).val != key)
{
var low: Int := 0
var high: Int := len(a)
index := -1
while (low < high)
invariant access(a) && untouched(a)
invariant 0 <= low && low <= high && high <= len(a)
invariant index == -1 ==> forall i: Int :: {loc(a, i)}(0 <= i && i < len(a) && !(low <= i && i < high)) ==> loc(a, i).val != key
invariant -1 <= index && index < len(a)
invariant 0 <= index ==> loc(a, index).val == key
{
var mid: Int := (low + high) \ 2
if (loc(a, mid).val < key) {
low := mid + 1
} else {
if (key < loc(a, mid).val) {
high := mid
} else {
index := mid
high := mid
}
}
}
}
/* Encoding of arrays */
field val: Int
domain IArray {
function loc(a: IArray, i: Int): Ref
function len(a: IArray): Int
function first(r: Ref): IArray
function second(r: Ref): Int
axiom all_diff {
forall a: IArray, i: Int :: {loc(a, i)}
first(loc(a, i)) == a && second(loc(a, i)) == i
}
axiom length_nonneg {
forall a: IArray :: len(a) >= 0
}
}