主页 / coding / 问题 / 77480353
Accepted
Drona Nagarajan
Asked: 2023-11-14 19:47:04 +0800 CST

证明非线性遍历在 Dafny 终止

  • 772

我在 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。但达夫尼未能用这个谓词进行推理。

有达夫尼经验的人的帮助是无价的！

dafny

1 个回答

  1. Best Answer

    您可以尝试以下定义。

    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
}

    最后我继续努力。我能够得到以下信息来验证。

    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;
    }
}

    理想情况下，您应该将假设移至方法要求中，或者更好地定义引理，以确保基于链接的这些陈述是排列。

    • 1

相关问题