Dafny 断言通过但引理失败答案

【问题标题】：Dafny assertion passes but lemma failsDafny 断言通过但引理失败
【发布时间】：2023-02-09 09:33:16
【问题描述】：

出于某种原因，dafny 报告说 PreorderTraversalChildrenAreLater 的确保条件可能并不总是成立，即使量化表达式始终成立......稍后在同一引理中。理想情况下，一旦我展示了存在 k，我就试图展示 root.repr 的所有子元素稍后将出现在 PreorderTraversal 中。 ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> forall child :: child in PreorderTraversal(root)[k].repr && child != PreorderTraversal(root)[k] ==> exists j :: k < j < |PreorderTraversal(root)| && PreorderTraversal(root)[j] == child

function PreorderTraversal(root: TreeNode): seq<TreeNode>
    reads root.repr
    requires root.Valid()
    ensures forall x :: x in root.repr ==> x in PreorderTraversal(root)
    ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> PreorderTraversal(root)[k] in root.repr && PreorderTraversal(root)[k].Valid()
    // ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> PreorderTraversal(root)[k] in root.repr
{
   if root.left != null && root.right != null then [root]+PreorderTraversal(root.left)+PreorderTraversal(root.right) else if root.left != null then [root]+PreorderTraversal(root.left) else if root.right != null then [root]+PreorderTraversal(root.right) else [root]
}

lemma {:verify true} PreorderTraversalChildrenAreLater(root: TreeNode)
    requires root.Valid()
    //the following does not verify
    ensures forall x :: x in root.repr ==> exists k: nat :: 0 <= k < |PreorderTraversal(root)| && PreorderTraversal(root)[k] == x
{
    // var what := PreorderTraversal(root);
    assert forall x :: x in root.repr ==> x in PreorderTraversal(root);
    forall x | x in root.repr 
        ensures exists k: nat :: 0 <= k < |PreorderTraversal(root)| && PreorderTraversal(root)[k] == x
    {
        assert x in PreorderTraversal(root);
        seqbusiness(PreorderTraversal(root), x);
    }
    // but it verifies here, at least I get the green checkmark
    assert forall x :: x in root.repr ==> exists k: nat :: 0 <= k < |PreorderTraversal(root)| && PreorderTraversal(root)[k] == x;
}

lemma seqbusiness<A>(s: seq<A>, elem: A)
    requires elem in s
    ensures exists k:nat :: 0 <= k < |s| && s[k] == elem
{

}

class TreeNode {
    var val: int;
    var left: TreeNode?;
    var right: TreeNode?;
    ghost var repr: set<TreeNode>;

    constructor(val: int, left: TreeNode?, right: TreeNode?)
        requires left != null ==> left.Valid()
        requires right != null ==> right.Valid()
        requires left != null && right != null ==> left.repr !! right.repr
        ensures this.val == val
        ensures this.left == left
        ensures this.right == right
        ensures left != null ==> this !in left.repr
        ensures right != null ==> this !in right.repr
        ensures Valid()
    {
        this.val := val;
        this.left := left;
        this.right := right;
        var leftRepr := if left != null then {left}+left.repr else {};
        var rightRepr := if right != null then {right}+right.repr else {};
        this.repr := {this} + leftRepr + rightRepr;
    }

    predicate Valid()
        reads this, repr
        decreases repr
    {
        this in repr &&
        (this.left != null ==>
        (this.left in repr
        && this !in this.left.repr
        && this.left.repr < repr
        && this.left.Valid()
        ))
        && (this.right != null ==>
        (this.right in repr
        && this !in this.right.repr
        && this.right.repr < repr
        && this.right.Valid())) &&
        (this.left != null && this.right != null ==> this.left.repr !! this.right.repr && this.repr == {this} + this.left.repr + this.right.repr)
        && (this.left != null && this.right == null ==> this.repr == {this} + this.left.repr)
        && (this.right != null && this.left == null ==> this.repr == {this} + this.right.repr)
        && (this.right == null && this.left == null ==> this.repr == {this})
    }
}

【问题讨论】：

标签： dafny

【解决方案1】：

我同意它没有按原样验证，也不清楚为什么。但是，我确实通过如下提出谓词来设法让它通过：

predicate WithinRootPreorder(root:TreeNode, x: TreeNode)
reads root.repr
requires root.Valid()
requires x in root.repr {
    exists k: nat :: 0 <= k < |PreorderTraversal(root)| && PreorderTraversal(root)[k] == x
}

lemma {:verify true} PreorderTraversalChildrenAreLater(root: TreeNode)
    //reads root.repr
    requires root.Valid()
    ensures root.repr == old(root.repr)
    //the following does not verify
    ensures forall x :: x in root.repr ==> WithinRootPreorder(root,x)
{
   ...
   assert forall x :: x in root.repr ==> WithinRootPreorder(root,x);
}

这似乎对我有用。

【讨论】：