Parallel Array Replace (Quantified Permissions)
Running example from the CAV'16 paper: replace each occurrence of an element in an array segment by recursing over the two half-segments in parallel.
define pre1(a, l, r) 0 <= l && l < r && r <= len(a)
define pre2(a, l, r) forall i: Int :: l <= i && i < r ==> acc(loc(a, i).val)
define post1(a, l, r) pre2(a, l, r)
define post2(a, l, r) forall i: Int :: l <= i && i < r ==>
(old(loc(a, i).val == from)
? loc(a, i).val == to
: loc(a, i).val == old(loc(a, i).val))
method Replace(a: Array, left: Int, right: Int, from: Int, to: Int)
requires pre1(a, left, right)
requires pre2(a, left, right)
ensures post1(a, left, right)
ensures post2(a, left, right)
{
if (right - left <= 1) {
if(loc(a, left).val == from) {
loc(a, left).val := to
}
} else {
var mid: Int := left + (right - left) \ 2
//fork-left
exhale pre1(a, left, mid)
exhale pre2(a, left, mid)
//fork-right
exhale pre1(a, mid, right)
exhale pre2(a, mid, right)
//join-left
inhale post1(a, left, mid)
inhale post2(a, left, mid)
//join-right
inhale post1(a, mid, right)
inhale post2(a, mid, right)
}
}
method Client(a: Array)
requires 1 < len(a)
requires forall i: Int :: 0 <= i && i < len(a) ==> acc(loc(a, i).val)
requires Contains(a, 5, 1)
{
Replace(a, 1, len(a), 5, 7)
assert Contains(a, 5, 1) // Requires function framing
}
function Contains(a: Array, v: Int, before: Int): Bool
requires 0 <= before && before <= len(a)
requires forall i: Int :: 0 <= i && i < before ==> acc(loc(a, i).val)
/* Encoding of arrays */
field val: Int
domain Array {
function loc(a: Array, i: Int): Ref
function len(a: Array): Int
function first(r: Ref): Array
function second(r: Ref): Int
axiom all_diff {
forall a: Array, i: Int :: {loc(a, i)}
first(loc(a, i)) == a && second(loc(a, i)) == i
}
axiom length_nonneg {
forall a: Array :: len(a) >= 0
}
}