Hello,
I'm continuing to work on the ArraySet example, which we've seen in a couple other posts. It involves threading a "free" list and a "used" list through an array and you can view it as a "toy" memory allocator. I use some ghost
sequence variables to describe these elements.
I'm at the trickiest bit, which involves swapping an element from one list to another. I have a "swap" function that does the operation, and should preserve the invariant. However, I'm having difficulty with Dafny timing out; I can split the postconditions
across
two swap functions and get it to work, but if I put everything together it appears to run aground. Here are the two swap functions:
method swap1(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
modifies this;
modifies nextArray;
requires seqOk(hd, bs);
requires |bs| > 0 ;
requires 0 <= split < |bs| ;
requires |bs| <= nextArray.Length;
requires 0 <= newSlot < nextArray.Length;
requires newSlot !in bs;
ensures |bs'| > 0 ;
// the properties I care about for seqOk
ensures nextArray != null;
ensures (forall i, j :: (0 <= i < |bs'| && 0 <= j < |bs'| && i != j) ==> bs'[i] != bs'[j]);
ensures (hd == -1 <==> |bs'| == 0) ;
ensures (forall j :: j in bs' ==> (j >= 0 && j < nextArray.Length));
ensures (|bs'| > 0 ==> ((hd == bs'[0])));
// need to prove the 'ensures' below separately or I time out; see swap2. The
// necessary assertions for proof are commented out below.
//
// ensures (nextArray[lastElem(bs')] == -1);
{
var splitLoc := bs[split];
nextArray[newSlot], nextArray[splitLoc] := nextArray[splitLoc], newSlot ;
//assert ((split == |bs|-1) ==> (nextArray[newSlot] == -1));
bs' := bs[..split+1] + [newSlot] + bs[split+1..];
//assert((split == |bs'|-1) ==> (nextArray[lastElem(bs')] == -1));
//assert (|bs'| > 0 ==> (nextArray[lastElem(bs')] == -1));
assert(bs'[split+1] == nextArray[bs'[split]]) ;
assert (forall j :: 1 <= j <= split ==> nextArray[bs'[j-1]] == bs'[j]);
assert (forall j :: split+1 < j < |bs'| ==> nextArray[bs'[j-1]] == bs'[j]);
assert (forall j :: 1 <= j < |bs'| ==> nextArray[bs'[j-1]] == bs'[j]);
assert (forall i, j :: (0 <= i < |bs'| && 0 <= j < |bs'| && i != j) ==> bs'[i] != bs'[j]);
assert ((hd == -1) == (|bs'| == 0)) ;
assert (forall j :: j in bs' ==> (j >= 0 && j < nextArray.Length));
assert (|bs'| > 0 ==> ((hd == bs'[0])));
}
method swap2(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
modifies this;
modifies nextArray;
requires seqOk(hd, bs);
requires |bs| > 0 ;
requires 0 <= split < |bs| ;
requires |bs| <= nextArray.Length;
requires 0 <= newSlot < nextArray.Length;
requires newSlot !in bs;
ensures |bs'| > 0 ;
ensures nextArray != null;
ensures 0 <= lastElem(bs') < nextArray.Length;
// this is the one I actually care about.
ensures (nextArray[lastElem(bs')] == -1);
{
var splitLoc := bs[split];
nextArray[newSlot], nextArray[splitLoc] := nextArray[splitLoc], newSlot ;
assert ((split == |bs|-1) ==> (nextArray[newSlot] == -1));
bs' := bs[..split+1] + [newSlot] + bs[split+1..];
assert((split == |bs'|-1) ==> (nextArray[lastElem(bs')] == -1));
assert (|bs'| > 0 ==> (nextArray[lastElem(bs')] == -1));
// yay!
}
The entire program is below. My guess is that as I add assertions for one conjunct, I'm accreting junk that is causing Dafny to go astray when trying to prove the other things. Is there any way to localize assertions as relevant only for one thread of proof?
Thanks again!
Mike
class ArraySet {
var elementArray : array<int>;
var nextArray: array<int>;
var usedHd: int;
var freeHd: int;
ghost var usedSeq: seq<int> ;
ghost var freeSeq: seq<int> ;
// Invariant for array creating a simple store. You can think of it as a grossly simplified
// memory allocator. Each memory location (array slot) is either part of a "free list" or a
// "used list". Both lists are threaded through the structure of the array. We used a
// variant of this structure for a high-speed encryption application.
predicate index_ok(index: int)
reads this;
reads nextArray ;
{
nextArray != null && index >= 0 && index < nextArray.Length
}
function lastElem(input: seq<int>) : int
requires |input| > 0;
{
input[|input| - 1]
}
predicate seqOk(hd: int, theSeq: seq<int>)
reads this;
reads nextArray;
{
nextArray != null &&
(forall i, j :: 0 <= i < j < |theSeq| ==> theSeq[i] != theSeq[j]) &&
(hd == -1 <==> |theSeq| == 0) &&
(forall j :: j in theSeq ==> j >= 0 && j < nextArray.Length) &&
(forall j :: 1 <= j < |theSeq| ==> nextArray[theSeq[j-1]] == theSeq[j]) &&
(|theSeq| > 0 ==> hd == theSeq[0] && nextArray[lastElem(theSeq)] == -1)
}
predicate arrayInv()
reads this;
reads nextArray;
reads elementArray;
{
nextArray != null &&
elementArray != null &&
(forall j :: 0 <= j < nextArray.Length ==> -1 <= nextArray[j] < nextArray.Length) &&
-1 <= freeHd < nextArray.Length &&
-1 <= usedHd < nextArray.Length &&
nextArray.Length == elementArray.Length &&
nextArray != elementArray &&
// usedSeq & freeSeq are well formed and correctly mapped to the nextArray
seqOk(usedHd, usedSeq) &&
seqOk(freeHd, freeSeq) &&
// sequences contain no duplications, are disjoint, and exhaustive
(forall j :: 0 <= j < nextArray.Length ==> j in usedSeq || j in freeSeq) &&
(forall j :: j in usedSeq ==> j !in freeSeq) &&
(forall j :: j in freeSeq ==> j !in usedSeq) &&
true
}
method init(size: int)
modifies this;
requires size > 0;
ensures nextArray != null;
ensures forall j :: 0 <= j < nextArray.Length ==> -1 <= nextArray[j] < nextArray.Length;
ensures arrayInv();
{
elementArray := new int[size];
nextArray := new int[size];
parallel (j | 0 <= j < nextArray.Length) {
nextArray[j] := if j < nextArray.Length - 1 then j + 1 else -1;
}
usedHd := -1;
freeHd := 0;
usedSeq := [];
var fs, i := [], 0;
while (i < nextArray.Length)
invariant 0 <= i <= nextArray.Length;
invariant |fs| == i;
invariant forall j :: 0 <= j < i ==> fs[j] == j;
{
fs, i := fs + [i], i + 1;
}
freeSeq := fs;
// lemma needed to make the postcondition go through:
assert forall j :: 0 <= j < nextArray.Length ==> freeSeq[j] == j ==> j in freeSeq;
}
method insertHd(n: int) returns (result: bool)
modifies this;
modifies nextArray;
modifies elementArray;
requires arrayInv();
ensures arrayInv();
{
var oldUsedHd : int;
if (freeHd != -1) {
// assign usedHd to freeHd; if I get rid of oldUsedHd (using parallel assignment), proof fails. Why?
oldUsedHd := usedHd;
usedHd, freeHd := freeHd, nextArray[freeHd];
nextArray[usedHd] := oldUsedHd;
// assign the next pointer of the first used element to the previous head of the used list
elementArray[usedHd] := n;
usedSeq := [freeSeq[0]] + usedSeq;
freeSeq := freeSeq[1..];
assert (|usedSeq| > 1 ==> nextArray[usedSeq[0]] == usedSeq[1]) ;
result := true;
} else {
result := false;
}
}
/*
swap: add the newSlot array location into the list represented by sequence bs.
Steps:
Find the location for insert (splitLoc),
update the next pointers, and
update the sequence to match.
Swap should preserve the seqOk invariant, but it times out when I try to
prove the pieces all at once. Temporarily, I am proving the conjuncts
separately with swap1 and swap2, but both these operations are destructive
of the heap, so this won't work for "real"; Dafny is able to prove the
pieces, but when I put them together, I think it gets overloaded by the volume
of information for each conjunct. I'm looking for a way to separate the
proof into separate paths of execution here.
*/
method swap1(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
// swap1 code HERE
method swap2(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
// swap2 code HERE
method insertTl(n: int) returns (result: bool)
modifies this;
modifies nextArray;
modifies elementArray;
requires arrayInv();
requires usedHd != -1;
{
// array location and sequence location for insert.
var al := usedHd;
ghost var sl := 0;
}
method insert(n: int) returns (result: bool)
modifies this;
modifies nextArray;
modifies elementArray;
requires arrayInv();
ensures arrayInv();
{
if (freeHd == -1) {
result := false;
return;
} else if (usedHd == -1 || n < elementArray[usedHd]) {
result := insertHd(n) ;
assert (arrayInv());
return;
} else {
// find location and perform a swap HERE.
return;
}
}
}