Dafny存在表达式处理引用类的子串谓词验证问题

我尝试在类上定义操作并证明其性质，编写了如下子串判断谓词：

//the following resolves the error with substring, but creates problems down the line
//predicate isSubstring<A(!new)>(sub: seq<A>, super: seq<A>) {
predicate isSubstring<A>(sub: seq<A>, super: seq<A>) {
    |sub| <= |super| && exists xs: seq<A> :: IsSuffix(xs, super) && sub <= xs
}

predicate IsSuffix<T>(xs: seq<T>, ys: seq<T>) {
    |xs| <= |ys| && xs == ys[|ys| - |xs|..]
}

但该谓词触发错误：

a exists expression involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters

我知道为类型参数A添加(!new)限制可解决该谓词的错误，但在后续编写的引理中又遇到问题：

lemma AllChildrenTraversalsAreSubstrings(root: TreeNode) 
    requires root.Valid()
    ensures forall x :: x in root.repr && x in PreorderTraversal(root) ==> isSubstring(PreorderTraversal(x), PreorderTraversal(root))
{
    forall x | x in root.repr && x in PreorderTraversal(root) 
        ensures isSubstring(PreorderTraversal(x), PreorderTraversal(root))
    {
        if x == root {

        }else if x == root.left || x == root.right {
           PreorderTraversalSubstrings(root); 
        }else {
            if root.left != null && x in root.left.repr {
                AllChildrenTraversalsAreSubstrings(root.left);
            }
            if root.right != null && x in root.right.repr {
                AllChildrenTraversalsAreSubstrings(root.right);
            }
        }
    }
}

该引理的forall确保语句触发错误：

type parameter (A) passed to predicate isSubstring must support no references (got TreeNode)

其余相关代码（前序遍历函数、子串引理、TreeNode类）如下：

function method PreorderTraversal(root: TreeNode): seq<TreeNode>
    reads root.repr
    requires root.Valid()
    // ensures forall x :: x in PreorderTraversal(root) ==> x.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 injectiveSeq(PreorderTraversal(root))
    ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> PreorderTraversal(root)[k] in root.repr
    // ensures forall k :: 0 <= k < |PreorderTraversal(root)| ==> forall child :: child in PreorderTraversal(root)[k].repr && child != child in PreorderTraversal(root)[k] ==> exists j :: k < j < |PreorderTraversal(root)| && PreorderTraversal(root)[j] == child
{
   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 PreorderTraversalSubstrings(root: TreeNode)
    requires root.Valid()
    ensures root.left != null ==> isSubstring(PreorderTraversal(root.left), PreorderTraversal(root))
    ensures root.right != null ==> isSubstring(PreorderTraversal(root.right), PreorderTraversal(root))
{
   if root.left != null && root.right != null {
    calc {
        PreorderTraversal(root);
        [root]+PreorderTraversal(root.left)+PreorderTraversal(root.right);
    }
    assert |PreorderTraversal(root.left)| < |PreorderTraversal(root)|;
    assert |PreorderTraversal(root.right)| < |PreorderTraversal(root)|;
    assert IsSuffix(PreorderTraversal(root.left)+PreorderTraversal(root.right), PreorderTraversal(root));
    assert IsSuffix(PreorderTraversal(root.right), PreorderTraversal(root));
    assert PreorderTraversal(root.left) <= PreorderTraversal(root.left)+PreorderTraversal(root.right);
   }else if root.left != null && root.right == null {
    calc {
        PreorderTraversal(root);
        [root]+PreorderTraversal(root.left);
    }
    assert |PreorderTraversal(root.left)| < |PreorderTraversal(root)|;
    assert IsSuffix(PreorderTraversal(root.left), PreorderTraversal(root));
   }else if root.left == null && root.right != null {
    calc {
        PreorderTraversal(root);
        [root]+PreorderTraversal(root.right);
    }
    assert |PreorderTraversal(root.right)| < |PreorderTraversal(root)|;
    assert IsSuffix(PreorderTraversal(root.right), PreorderTraversal(root));
   }
}

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

奇怪的是，PreorderTraversalSubstrings在添加(!new)限制后可正常验证，但AllChildrenTraversalsAreSubstrings的forall确保语句仍报错。我该如何推进？切换到数据类型会更简单，但我要验证基于类的程序，是否可以定义二叉树数据类型并断言其操作与合法类树等价？若存在量词表达式不能引用已分配值，这种等价性是否可行？

1. 修复isSubstring谓词的类型限制问题 #

问题核心在于(!new)约束要求类型不能包含引用，但TreeNode是引用类型，无法满足该约束。因此需要重新定义isSubstring，避免使用依赖已分配引用集的存在量词。

可以直接用子串的标准定义改写谓词，不需要引入中间序列xs：

predicate isSubstring<A>(sub: seq<A>, super: seq<A>) {
    |sub| <= |super| && exists i: nat :: i + |sub| <= |super| && sub == super[i..i+|sub|]
}

这个定义直接检查是否存在起始索引i，使得super从i开始的子序列等于sub，完全避开了原定义中存在量词依赖引用类型序列的问题，也就不需要(!new)约束了。

2. 修复AllChildrenTraversalsAreSubstrings引理的验证问题 #

原引理的结构可以保留，但需要补充断言来链接递归调用和目标结论：

lemma AllChildrenTraversalsAreSubstrings(root: TreeNode) 
    requires root.Valid()
    ensures forall x :: x in root.repr ==> isSubstring(PreorderTraversal(x), PreorderTraversal(root))
{
    forall x | x in root.repr 
        ensures isSubstring(PreorderTraversal(x), PreorderTraversal(root))
    {
        if x == root {
            // 根节点的遍历序列是自身的子串，显然成立
            assert PreorderTraversal(x) == PreorderTraversal(root);
        } else if root.left != null && x in root.left.repr {
            AllChildrenTraversalsAreSubstrings(root.left);
            // 利用前序遍历的结构：root的序列是[root] + left序列 + right序列
            calc {
                PreorderTraversal(root);
                [root] + PreorderTraversal(root.left) + (if root.right != null then PreorderTraversal(root.right) else []);
            }
            // 递归得到x的遍历序列是left序列的子串，因此也是root序列的子串
            assert isSubstring(PreorderTraversal(x), PreorderTraversal(root.left));
            assert isSubstring(PreorderTraversal(x), [root] + PreorderTraversal(root.left) + (if root.right != null then PreorderTraversal(root.right) else []));
        } else if root.right != null && x in root.right.repr {
            AllChildrenTraversalsAreSubstrings(root.right);
            calc {
                PreorderTraversal(root);
                [root] + (if root.left != null then PreorderTraversal(root.left) else []) + PreorderTraversal(root.right);
            }
            assert isSubstring(PreorderTraversal(x), PreorderTraversal(root.right));
            assert isSubstring(PreorderTraversal(x), [root] + (if root.left != null then PreorderTraversal(root.left) else []) + PreorderTraversal(root.right));
        }
    }
}

另外，原引理的ensures条件中x in PreorderTraversal(root)是冗余的，因为PreorderTraversal的后置条件已经保证x in root.repr就必然在遍历序列中，可以去掉。

3. 关于类树与数据类型树的等价性验证 #

如果一定要用数据类型来辅助验证，是可行的：

• 首先定义二叉树数据类型：

  datatype Tree = Leaf(int) | Node(int, Tree, Tree)
  

• 然后定义从合法TreeNode类实例到Tree数据类型的转换函数，同时证明该转换的正确性（比如遍历结果一致、结构对应等）。
• 由于数据类型的值不涉及引用分配，原有的子串谓词（甚至带(!new)的版本）都可以直接使用，先在数据类型上证明性质，再通过等价性转换映射到类实例上。

这种等价性验证不受存在量词的限制，因为转换函数是纯函数（不涉及引用状态），可以安全地在断言中使用，将类的性质证明转化为数据类型的性质证明，降低验证难度。

内容的提问来源于stack exchange，提问作者Hath995