I have an array of nats in Dafny that I want to traverse in a non-linear manner. To elucidate the problem: Consider an array such that (please ignore the syntax for now):
var links : array<nat>;
links := [1,2,5,4,0,3];
At a given index 'i', links[i] holds the index of the next element that must be considered. Here, let i == 2 ==> links[i] == 5. In the next iteration, the loop reads the value at index 5 which is 3 and so on till links[i] == 0.
I have implemented a while loop and some predicates that do not seem to prove termination.
The first predicate is that every element in the list is unique and no element is greater than the length of the loop. This is so because otherwise the array becomes circular. The predicate comes from here.
forall i, j | 0 <= i < links.Length && 0 <= j < links.Length && i != j :: links[i] != links[j]
The second predicate is that there exists an element in the array which is 0. This is the terminating condition.
exists q :: 0 <= q < links.Length && links[q] == 0
The while loop iterates as follows:
qAct = links[0];
while(qAct != 0)
/* invariants and decreases ??? */
{
qAct = links[qAct];
}
The problem here is that qAct does not really decrease. To remedy that, I reasoned that the loop will never iterate more than its length, so I tried:
qAct = links[0];
var i : nat;
i := 0
while(qAct != 0 && i < links.Length)
/* this terminates */
decreases links.Length - i
{
qAct := links[qAct];
i := i + 1;
}
The reasoning is that, as per the design of the array, the number of elements cannot be greater than the length of the array. Therefore, the loop iterates at most links.Length times.
Is there way to prove the termination without using "i"? I also tried defining "i" as a ghost variable but I get an error saying "assignment to non-ghost variable is not allowed in this context." at qAct := links[qAct].
A pen and paper proof with Hoare logic (and simple reasoning) is enough to show that qAct eventually converges to 0 due the second predicate. But Dafny fails to reason with this predicate.
Help from people experienced with Dafny is invaluable!
You might try the following definitions.
predicate derangement(s: seq<nat>) {
forall i :: 0 <= i < |s| ==> s[i] != i
}
predicate permutation(s: seq<nat>) {
forall i :: 0 <= i < |s| ==> i in s
}
method test(anotherPerm: seq<nat>)
requires permutation(anotherPerm) && derangement(anotherPerm)
{
var tests := [2,0,1];
var tests2 := [0,1,2];
assert derangement(tests);
assert permutation(tests);
assert permutation(tests2);
// assert !derangement(tests2); //this will actually not verify despite being true
}
In the end I kept working on it. I was able to get the following to verify.
predicate derangement(s: seq<nat>) {
forall i :: 0 <= i < |s| ==> s[i] != i
}
predicate permutation(s: seq<nat>) {
forall i :: 0 <= i < |s| ==> i in s
}
function multisetRange(n: nat): multiset<nat> {
multiset(seq(n, i => i))
}
predicate distinct<A(==)>(s: seq<A>) {
forall x,y :: x != y && 0 <= x <= y < |s| ==> s[x] != s[y]
}
method test() {
var tests := [2,0,1];
var tests2 := [0,1,2];
var t4 := seq(3, i => i);
var test3 := multisetRange(3);
assert t4 == tests2;
assert 0 in t4;
assert 0 in test3;
assert multiset(tests) == multisetRange(3);
assert derangement(tests);
assert permutation(tests);
assert permutation(tests2);
// assert !derangement(tests2);
}
method {:timelimit 40} end(links: seq<nat>)
requires |links| > 0
requires permutation(links)
requires derangement(links)
requires distinct(links)
{
assume forall x :: x in links ==> 0 <= x < |links|;
assume forall x :: x in links ==> multiset(links)[x] ==1;
// assume multiset(links) == multisetRange(|links|);
var qAct: nat := links[0];
assert links[0] in links;
var i : nat := 0;
ghost var oldIndex := 0;
ghost var indices: multiset<nat> := multiset{0};
ghost var visited: multiset<nat> := multiset{};
while qAct != 0
invariant 0 <= oldIndex < |links|
invariant qAct == links[oldIndex]
invariant oldIndex in indices
invariant qAct in links
invariant indices == visited + multiset{0}
invariant forall x :: x in visited ==> exists k :: 0 <= k < |links| && links[k] == x && k in indices
invariant qAct !in visited
invariant 0 <= qAct < |links|
decreases multiset(links) - visited
{
ghost var oldVisit := visited;
ghost var oldqAct := qAct;
ghost var oldOldIndex := oldIndex;
oldIndex := qAct;
visited := visited + multiset{qAct};
indices := indices + multiset{qAct};
assert oldqAct in visited;
assert forall x :: x in visited ==> exists k :: 0 <= k < |links| && links[k] == x && k in indices by {
forall x | x in visited
ensures exists k :: 0 <= k < |links| && links[k] == x && k in indices
{
if x == oldqAct {
assert links[oldOldIndex] == oldqAct;
assert exists k :: 0 <= k < |links| && links[k] == x && k in indices;
}else {
assert x in oldVisit;
assert exists k :: 0 <= k < |links| && links[k] == x && k in indices;
}
}
}
qAct := links[qAct];
i := i + 1;
}
}
Ideally you should either move the assume's into the method requirement or better yet define lemmas that ensure those statements based on the links being a permutation.