Array Max, straight-forward (Quantified Permissions)
Finding the maximum in an array the straight-forward way
/* Finding the maximum in an array.
* See also http://verifythus.cost-ic0701.org/common-example/
*/
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)
define is_max(i, a, u) forall j: Int :: 0 <= j && j < u ==> loc(a, j).val <= loc(a, i).val
/* Note: Returns the position of the array maximum (and not the maximum itself) to
* avoid the need for an existential in the postcondition (and the loop invariant)
* that states that there exists an index into the array at which the maximum can
* be found.
*/
method max(a: IArray) returns (at: Int)
requires access(a)
ensures access(a) && untouched(a)
ensures len(a) == 0 ? at == -1 : (0 <= at && at < len(a))
ensures is_max(at, a, len(a))
{
if (len(a) == 0) {
at := -1
} else {
at := 0
var k: Int := 1
while (k < len(a))
invariant 1 <= k && k <= len(a)
invariant access(a) && untouched(a)
invariant 0 <= at && at < k
invariant is_max(at, a, k)
{
if (loc(a, at).val < loc(a, k).val) {
at := k
}
k := k + 1
}
}
}
method client() {
var a: IArray
inhale len(a) == 3
inhale access(a)
inhale forall i: Int :: 0 <= i && i < len(a) ==> loc(a, i).val == i
var x: Int
x := max(a)
assert loc(a, 0).val <= x
assert x == loc(a, len(a) - 1).val /* Necessary to prove the final assertion (due to triggering) */
assert x == 2
assert loc(a, 1).val < x
}
/* 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
}
}