Quickselect (Quantified Permissions)
An encoding of the Quickselect algorithm over arrays
/* https://en.wikipedia.org/wiki/Quickselect
*
* Changes w.r.t. the wikipedia code:
* - Select returns the index of the n-th smallest element, not the element
* itself
* - In order to be able to specify that an array has been permuted by
* certain operations, the permutation witness (pw) is made explicit
* (Leino, Monahan - Dafny meets the Verification Benchmarks Challenge)
*/
method swap(a: IArray, i: Int, j: Int)
requires 0 <= i && i < len(a)
requires 0 <= j && j < len(a)
requires acc(loc(a, i).val)
requires i != j ==> acc(loc(a, j).val)
ensures acc(loc(a, i).val)
ensures i != j ==> acc(loc(a, j).val)
ensures loc(a, i).val == old(loc(a, j).val)
ensures loc(a, j).val == old(loc(a, i).val)
{
var t: Int := loc(a, i).val
loc(a, i).val := loc(a, j).val
loc(a, j).val := t
}
/* permuted(a, left, pw) says that the element that is now at a[i] was originally
* at a[pw[i]].
*
* Technical detail: The explicit trigger {pw[i]} is necessary, the axiom might
* otherwise yield a matching loop if the trigger {loc(a, i)} is picked (by
* Silver or Z3). In that case, instantiating the axiom with loc(a, N) will
* yield the term loc(a, pw[N])(ignoring old), which can be used to trigger the
* axiom again, causing a matching loop.
*/
define permuted(a, left, right, pw)
forall i: Int :: {pw[i]} left <= i && i <= right ==> loc(a, i).val == old(loc(a, pw[i]).val)
method partition(a: IArray, left: Int, right: Int, pivotIndex: Int) returns (storeIndex: Int, pw: Seq[Int])
/* All indices are valid and their relative order is satisfied */
requires 0 <= left && left < right && right < len(a)
requires left <= pivotIndex && pivotIndex <= right
/* Permissions to the array segment with indices [left..right] */
requires forall i: Int :: left <= i && i <= right ==> acc(loc(a, i).val)
/* Returned index is a valid index */
ensures left <= storeIndex && storeIndex <= right
/* Return all taken permissions */
ensures forall i: Int :: left <= i && i <= right ==> acc(loc(a, i).val)
/* The pivot element is now stored at a[storeIndex] */
ensures loc(a, storeIndex).val == old(loc(a, pivotIndex).val)
/* All elements left (right) of the pivot are smaller than (at least as big as) the pivot */
ensures forall i: Int :: left <= i && i < storeIndex ==> loc(a, i).val < loc(a, storeIndex).val
ensures forall i: Int :: storeIndex < i && i <= right ==> loc(a, storeIndex).val <= loc(a, i).val
/* pw witnesses a permutation of the array segment */
ensures |pw| == right + 1
ensures forall i: Int :: left <= i && i <= right ==> left <= pw[i] && pw[i] <= right
ensures forall i: Int, k: Int :: left <= i && i < k && k <= right ==> pw[i] != pw[k]
/* The array segment has been permuted */
ensures permuted(a, left, right, pw)
{
var pivotValue: Int := loc(a, pivotIndex).val
/* Initialize pw */
pw := [0..right + 1)
/* Alternative:
* inhale |pw| == right + 1
* inhale forall i: Int :: left <= i && i <= right ==> pw[i] == i
*/
swap(a, pivotIndex, right) /* Move pivot to end, i.e. it is now at a[right] */
/* Swap pw[pivotIndex] and pw[right], which corresponds to
* swapping a[pivotIndex] and a[right]
*/
pw := pw[pivotIndex := pw[right]]
[right := pw[pivotIndex]]
storeIndex := left
var j: Int := left
while (j < right)
/* All indices are valid and their relative order is satisfied */
invariant left <= j && j <= right
invariant left <= storeIndex && storeIndex <= j
/* Permissions to the array segment.
* NOTE: Permissions to a[left..right) would suffice, and it would preserve
* information about the location of the pivot element, i.e. it would make
* invariant INV-PIV unnecessary. The current invariant, however, makes it
* possible to re-use the permuted(...) assertion.
*/
invariant forall i: Int :: left <= i && i <= right ==> acc(loc(a, i).val)
invariant loc(a, right).val == pivotValue /* INV-PIV */
/* All elements left (right) of the pivot are smaller than (at least as big as) the pivot */
invariant forall i: Int :: left <= i && i < storeIndex ==> loc(a, i).val < pivotValue
invariant forall i: Int :: storeIndex <= i && i < j ==> pivotValue <= loc(a, i).val
/* pw witnesses a permutation of the already visited array segment */
invariant |pw| == right + 1
invariant forall i: Int :: left <= i && i <= right ==> left <= pw[i] && pw[i] <= right
invariant forall i: Int, k: Int :: left <= i && i < k && k <= right ==> pw[i] != pw[k]
/* The array segment has been permuted */
invariant permuted(a, left, right, pw)
{
if (loc(a, j).val < pivotValue) {
swap(a, j, storeIndex)
/* Swap pw[storeIndex] and pw[j], which corresponds to
* swapping a[storeIndex] and a[j]
*/
pw := pw[storeIndex := pw[j]]
[j := pw[storeIndex]]
storeIndex := storeIndex + 1
}
j := j + 1
}
swap(a, right, storeIndex) /* Move pivot to its final position */
/* Update permutation witness accordingly */
pw := pw[storeIndex := pw[right]]
[right := pw[storeIndex]]
}
method select_rec(a: IArray, left: Int, right: Int, n: Int) returns (storeIndex: Int, pw: Seq[Int])
/* All indices are valid and their relative order is satisfied */
requires 0 <= left && left <= right && right < len(a)
requires left <= n && n <= right
/* Permissions to the array segment with indices [left..right] */
requires forall i: Int :: left <= i && i <= right ==> acc(loc(a, i).val)
/* Returned index is a valid index */
ensures left <= storeIndex && storeIndex <= right
/* Return all taken permissions */
ensures forall i: Int :: left <= i && i <= right ==> acc(loc(a, i).val)
/* From P1 and P2 it follows that loc(a, storeIndex).val is the n-th smallest element */
ensures storeIndex == n /* P1 */
ensures forall i: Int :: left <= i && i < storeIndex ==> loc(a, i).val <= loc(a, storeIndex).val /* P2 */
ensures forall i: Int :: storeIndex < i && i <= right ==> loc(a, storeIndex).val <= loc(a, i).val /* P3 */
/* pw witnesses a permutation of the array segment */
ensures |pw| == right + 1
ensures forall i: Int :: left <= i && i <= right ==> left <= pw[i] && pw[i] <= right
ensures forall i: Int, j: Int :: left <= i && i < j && j <= right ==> pw[i] != pw[j]
/* The array segment has been permuted */
ensures permuted(a, left, right, pw)
{
var pwPar: Seq[Int]
var pwRec: Seq[Int]
if (left == right) {
/* If the list contains only one element, return it */
storeIndex := left
pw := [0..left + 1)
} else {
var pivotIndex: Int
inhale left <= pivotIndex && pivotIndex <= right /* Non-det. choose a pivot index */
pivotIndex, pwPar := partition(a, left, right, pivotIndex)
if (n == pivotIndex) {
storeIndex := pivotIndex
pw := pwPar
} elseif (n < pivotIndex) {
storeIndex, pwRec := select_rec(a, left, pivotIndex - 1, n)
/* In order to prove P3, we need to know that
* loc(a, storeIndex).val <= loc(a, pivotIndex).val
* This follows from the fact that the array segment a[left..pivotIndex - 1]
* has been permuted, as witnessed by pw.
* Concluding this (currently) needs to be triggered explicitly by the
* following assertion.
*/
assert dummy(pwRec[storeIndex])
/* Recall that pw should witness that the element that is now at a[i] previously
* was at a[pw[i]]
*
* Up to this point
* 1. the call to partition permuted a[left..right],
* witnessed by pwPar
* 2. the recursive call to select_rec permuted a[left..pivotIndex - 1],
* witnessed by pwRec
*
* Hence, an element that is now at a[i] previously was at
* - a[pwPar[pwRec[i]]] if left <= i <= pivotIndex - 1
* - a[pwPar[i]] if pivotIndex <= i <= right
*/
inhale |pw| == right + 1
inhale forall i: Int :: left <= i && i <= pivotIndex - 1 ==> pw[i] == pwPar[pwRec[i]]
inhale forall i: Int :: pivotIndex <= i && i <= right ==> pw[i] == pwPar[i]
} else {
/* Analogous to the previous case, but affecting a[pivotIndex + 1..right] */
storeIndex, pwRec := select_rec(a, pivotIndex + 1, right, n)
assert dummy(pwRec[storeIndex])
inhale |pw| == right + 1
inhale forall i: Int :: left <= i && i <= pivotIndex ==> pw[i] == pwPar[i]
inhale forall i: Int :: pivotIndex + 1 <= i && i <= right ==> pw[i] == pwPar[pwRec[i]]
}
}
}
method client(a: IArray)
requires 10 < len(a)
requires forall i: Int :: 0 <= i && i < len(a) ==> acc(loc(a, i).val)
requires forall i: Int :: 0 <= i && i <= 10 ==> loc(a, i).val == i
ensures forall i: Int :: 0 <= i && i < len(a) ==> acc(loc(a, i).val)
{
var storeIndex: Int
var pw: Seq[Int]
storeIndex, pw := select_rec(a, 0, 10, 3)
assert storeIndex == 3
assert loc(a, storeIndex).val == old(loc(a, pw[storeIndex]).val)
assert old(loc(a, 0).val) == 0
assert old(loc(a, 3).val) == 3
assert old(loc(a, 2).val) != old(loc(a, 3).val)
/* Cannot been proven (directly, yet) */
//assert loc(a, storeIndex).val == 3
//assert loc(a, 2).val != loc(a, 3).val
}
/* 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
}
}
/* Misc */
function dummy(i: Int): Bool { true }