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.
In the end I kept working on it. I was able to get the following to verify.
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.