Dafny 修改子句和可为空的字段

Question

框架系统有很多问题。试图验证另一个leetcode问题，本质上是树的左右节点交换到位。试图将其作为对象方法和独立函数来解决。

独立函数的问题是它抱怨递归调用可能违反了上下文的修改子句。我将我能想到的所有内容都添加到修改子句中，但它仍然不起作用。我觉得归纳应该足够了。

/**
 * https://leetcode.com/problems/invert-binary-tree/description/
 * Definition for a binary tree node.
 * class TreeNode {
 *     val: number
 *     left: TreeNode | null
 *     right: TreeNode | null
 *     constructor(val?: number, left?: TreeNode | null, right?: TreeNode | null) {
 *         this.val = (val===undefined ? 0 : val)
 *         this.left = (left===undefined ? null : left)
 *         this.right = (right===undefined ? null : right)
 *     }
 * }

function invertTree(root: TreeNode | null): TreeNode | null {
    if(root == null) return null;
    let leftChild = invertTree(root.left);
    let rightChild = invertTree(root.right);
    root.right = leftChild;
    root.left = rightChild;
    return 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)
    }

}

method  invertBinaryTree(root: TreeNode?) returns (newRoot: TreeNode?)
    modifies {root} + (if root != null && root.left != null then {root.left} else {}) + (if root != null && root.right != null then {root.right} else {})
    requires root != null ==> root.Valid()
    ensures root != null ==> newRoot == root && newRoot.right == old(root.left) && root.left == old(root.right)
    ensures root == null ==> newRoot == null
    ensures root != null ==> newRoot != null && newRoot.repr == root.repr && newRoot.Valid()
    decreases if root == null then {} else root.repr
{
    if root != null {
        assert root in root.repr;
        assert root.Valid();
        var leftChild := null;
        if root.left != null {
            assert root.left != null;
            assert root.left.repr < root.repr;
            assert root.left.Valid();
            leftChild := invertBinaryTree(root.left);
        }
        var rightChild := root.right;
        if root.right != null  {
            assert root.right.Valid();
            rightChild := invertBinaryTree(root.right);
        }

        root.right := leftChild;
        root.left := rightChild;
        return root;
    }else{
        return null;
    }
}

Answer 1

您的 modifies 子句没有考虑到该方法是递归的。所以你不仅需要说明你在递归的顶层修改了什么，还需要说明所有可能的递归调用将修改什么。

我相信类似的东西

modifies if root != null then root.repr else {}

应该为你工作。