Dafny谓词isBinarySearchTree

Question

我必须用Dafny写一个BST (二进制搜索树)类。

我从Dafny开始，然后编写一个类，插入方法是最简单的部分。

我多次尝试编写递归谓词，该谓词可以检查作为参数传递的树是否为BST (没有平衡条件，遵循规则left.value < node.value && right.value >node.value的简单二叉树)。

我在另一个StackOverflow post中找到了一种方法来实现它，在谓词中传递函数，主递归检查在函数中，但它似乎不起作用。

该错误基本上是“此调用的预条件可能不成立”。

以下是代码：

datatype Tree = Nil | Node(left: Tree, value: int, right: Tree)

class TreeADT{  

    function isBST(tree: Tree): bool
        decreases tree
    {
        match tree
        case Nil => true
        case Node(_,_,_) =>
            (tree.left == Nil || tree.left.value < tree.value) 
            && (tree.right == Nil || tree.right.value > tree.value) 
            && isBST(tree.left) && isBST(tree.right)
    }

    predicate isBinarySearchTree(tree: Tree)
    {
        isBST(tree)
    }
    
    method insert(tree: Tree, value: int) returns (toAdd: Tree) //maybe remove
        requires isBinarySearchTree(tree) 
        decreases tree;
        // ensures isBinarySearchTree(toAdd) //same error appear here
    {
        if(tree == Nil) {return Node(Nil, value, Nil);}
        else{
            if(value == tree.value) {return tree;}
            var temp: Tree;
            if(value < tree.value){
                temp := insert(tree.left, value);
                toAdd := Node(temp, tree.value, tree.right);
            }else{
                temp := insert(tree.right, value);
                toAdd := Node(tree.left, tree.value, temp);
            }
            return toAdd;
        }
            
    }

    method printOrderedTree(tree:Tree)
        decreases tree
    {
        if tree == Nil {}
        else { 
            printOrderedTree(tree.left); 
            print tree.value, ", "; 
            printOrderedTree(tree.right);
        }
    }


    method Main() {
        var t := insert(Nil, 5);
        var u := insert(t, 2); // error on pre-condition here
        print t, "\n";
        print u, "\n";
        printOrderedTree(u);
        var b:bool := isBST(u);
    }
}

我还试图完全在谓词中完成，但递归检查似乎无论如何都不起作用。

在谓词中得到递归检查而不是循环检查，有什么想法吗？

感谢您的阅读。

编辑：

按照James的回答，我修改了我的代码

datatype Tree = Nil | Node(left: Tree, value: int, right: Tree)

predicate isBinarySearchTree(tree: Tree)
    decreases tree
{
    match tree
    case Nil => true
    case Node(_,_,_) =>
        (tree.left == Nil || tree.left.value < tree.value) 
        && (tree.right == Nil || tree.right.value > tree.value) 
        && isBinarySearchTree(tree.left) && isBinarySearchTree(tree.right)
        && treeMin(tree.value, tree.right) && treeMax(tree.value, tree.left)
}

predicate treeMax(max: int, tree: Tree)
    decreases tree
{
    match tree
    case Nil => true
    case Node(left,v,right) => (max > v) && treeMax(max, left) && treeMax(max, right)
}

predicate treeMin(min: int, tree:Tree)
    decreases tree
{
    match tree
    case Nil => true
    case Node(left,v,right) => (min < v) && treeMin(min, left) && treeMin(min, right)
}

method insert(tree: Tree, value: int) returns (toAdd: Tree) //maybe remove
    requires isBinarySearchTree(tree) 
    decreases tree;
    ensures isBinarySearchTree(toAdd)
{
    if(tree == Nil) {return Node(Nil, value, Nil);}
    else{
        if(value == tree.value) {return tree;}
        var temp: Tree;
        if(value < tree.value){
            temp := insert(tree.left, value);
            toAdd := Node(temp, tree.value, tree.right);
        }else{
            temp := insert(tree.right, value);
            toAdd := Node(tree.left, tree.value, temp);
        }
        return toAdd;
    }
        
}

method printOrderedTree(tree:Tree)
    decreases tree
{
    if tree == Nil {}
    else { 
        printOrderedTree(tree.left); 
        print tree.value, ", "; 
        printOrderedTree(tree.right);
    }
}


method Main() {
    var t := insert(Nil, 5);
    var u := insert(t, 2);
    print t, "\n";
    print u, "\n";
    u := insert(u, 1);
    u := insert(u, 3);
    u := insert(u, 7);
    u := insert(u, 6);
    u := insert(u, 4);
    printOrderedTree(u);
}

但是，在requires语句中也会出现同样的问题，我现在检查左侧的所有值是否较小，而右侧的值是否都更大，但此错误再次发生。

A postcondition might not hold on this return path.

如果我注释掉了ensures语句，就会得到以下错误：

A precondition for this call might not hold.

所有的构造，想法和愚蠢的提示将被仔细阅读。

谢谢。

Answer 1

您的代码有几个问题。

(1) TreeADT类的用途是什么？在Dafny中，类通常用于表示可变对象，但是您的类没有字段或mutator方法，您可以使用datatype来保存数据，这样就可以完全摆脱类。

(2)你对isBST的定义是错误的。下面是一个示例：

method UhOh()
  ensures isBST(Node(Node(Nil, 3, Node(Nil, 7, Nil)), 5, Nil))
{}

这棵树不是二进位搜索树，因为7大于5，但7在5的左边子树中。但是你的定义允许这棵树。

(3)您遇到的具体问题是，Dafny无法证明t中的变量Main是二进制搜索树。我看你把insert的后置条件注释掉了。为什么？你需要那个后置条件。

我也不知道您所说的“在谓词中传递函数”是什么意思。您有一个无用的(尽管无害)包装谓词isBST。在Dafny中，单词predicate只不过是返回类型为bool的function的缩写。

您编辑的代码看起来好多了。现在，insert的这两个附加的后置条件就足以完成这个证明了：

ensures forall x :: treeMin(x, tree) && x < value ==> treeMin(x, toAdd)
ensures forall x :: treeMax(x, tree) && x > value ==> treeMax(x, toAdd)

Answer 2

添加了几个assert语句之后，您可以看到dafny无法验证什么。

   if (value < tree.value) {
        temp := insert(tree.left, value);
        toAdd := Node(temp, tree.value, tree.right);
        assert treeMax(tree.value, temp);
    }
    else {
        temp := insert(tree.right, value);
        toAdd := Node(tree.left, tree.value, temp);
        assert treeMin(tree.value, temp);
    }

达夫尼无法验证添加的断言持有。思考dafny无法验证的原因是，它抽象地看起来所有的方法都有给定的前后条件，忘记了实现。insert方法的前提条件是输入是有效二叉树，后置条件是输出有效二叉树。因此，插入方法，它总是返回树下面，例如，是有效的实现。

​

​

现在不难理解为什么treeMax或treeMin在temp总是Tree(Tree(Nil, 1, Nil), 3, Tree(Nil, 5, Nil))时不起作用。

回顾过去，更大的问题是ensures提供的输入树和输出树之间没有联系。