Dafny 谓词 isBinarySearchTree

Posted 2023-03-16

【中文标题】Dafny 谓词 isBinarySearchTree

【英文标题】：Dafny predicate isBinarySearchTree

【发布时间】：2021-12-22 05:42:21

【问题描述】：

我必须在 Dafny 中编写一个小 BST（二叉搜索树）类。 我从 Dafny 开始，然后编写一个类，插入方法是最简单的部分。

我多次尝试编写一个递归谓词，它可以检查作为参数传递的树是否是 BST（没有平衡条件，遵循规则 left.value 节点的简单二叉树。值）。

我在另一个 *** 帖子中发现了一种在谓词中传递函数的方法，并且主要的递归检查在函数中，但它似乎不起作用。

错误基本上是“此调用的先决条件可能不成立”。 代码如下：

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

我也尝试完全在谓词中执行此操作，但递归检查似乎无论如何都不起作用。

有没有办法在谓词中进行递归检查而不是循环检查？

感谢阅读。

编辑： 按照詹姆斯的回答，我修改了我的代码

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 和 Ensure 语句中，我现在检查是否左侧的所有值都较小，右侧的所有值都较大，但此错误再次发生

A postcondition might not hold on this return path.

如果我注释掉 Ensure 语句，我会收到以下错误：

A precondition for this call might not hold.

将认真阅读所有建设性的想法和愚蠢的提示。

谢谢。

【参考方案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 无法证明 Main 中的变量 t 是二叉搜索树。我看到您已将 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)

【讨论】：

我知道我对如何检查二叉搜索树的定义确实不好，我很欣赏你的回答，它指导我更好地使用 Dafny。 :) 但我的问题更关心如何在谓词中进行递归，并在 a && b &&... && c 这样的逻辑表达式中使用此递归的布尔返回但再次感谢这些信息 :)

@RainMaker 抱歉，我错过了一段时间——我编辑了我的答案以响应您的编辑

【参考方案2】：

添加几个断言语句后，您可以看到 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 无法验证添加的断言保留。思考为什么 dafny 无法验证的方法是，它看起来抽象的所有方法都具有给定的前置和后置条件而忘记了实现。 insert 方法前置条件是输入是有效的二叉搜索树，后置条件是输出是有效的二叉树。因此，例如始终返回树下的插入方法是有效的实现。

现在不难看出为什么当 temp 始终为 Tree(Tree(Nil, 1, Nil), 3, Tree(Nil, 5, Nil)) 时 treeMax 或 treeMin 将不成立。

回顾更大的问题是ensures提供的输入树和输出树之间没有链接。