我在 Dafny 有一个 nat 数组，我想以非线性方式遍历它。为了阐明问题：考虑一个数组，这样（请暂时忽略语法）：
var links : array<nat>;
links := [1,2,5,4,0,3];
在给定索引“i”处，links[i]保存必须考虑的下一个元素的索引。在这里，让i == 2 ==> links[i] == 5. 在下一次迭代中，循环读取索引 5 处的值，即 3，依此类推，直到links[i] == 0。
我已经实现了 while 循环和一些似乎无法证明终止的谓词。
第一个谓词是列表中的每个元素都是唯一的，并且没有元素大于循环的长度。之所以如此，是因为否则数组就会变成圆形。谓词来自这里。
forall i, j | 0 <= i < links.Length && 0 <= j < links.Length && i != j :: links[i] != links[j]
第二个谓词是数组中存在一个元素为 0。这是终止条件。
exists q :: 0 <= q < links.Length && links[q] == 0
while 循环迭代如下：
qAct = links[0];
while(qAct != 0)
/* invariants and decreases ??? */
{
qAct = links[qAct];
}
这里的问题是 qAct 并没有真正减少。为了解决这个问题，我推断循环的迭代永远不会超过其长度，所以我尝试：
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;
}
原因是，根据数组的设计，元素的数量不能大于数组的长度。因此，循环最多迭代 links.Length 次。
有没有办法在不使用“i”的情况下证明终止？我还尝试将“i”定义为幽灵变量，但收到一条错误消息“在此上下文中不允许分配给非幽灵变量”。在qAct := links[qAct]。
带有霍尔逻辑（和简单推理）的笔和纸证明足以表明 qAct 由于第二个谓词最终收敛到 0。但达夫尼未能用这个谓词进行推理。
有达夫尼经验的人的帮助是无价的！