Dafny謂詞isBinarySearchTree-有解無憂

我必須在 Dafny 中撰寫一個小 BST（二叉搜索樹）類。
我從 Dafny 開始，然后撰寫一個類，插入方法是最簡單的部分。

我多次嘗試撰寫一個遞回謂詞，它可以檢查作為引數傳遞的樹是否是 BST（沒有平衡條件，遵循 left.value < node.value && right.value > node.value 規則的簡單二叉樹）。

我在另一個 StackOverflow 帖子中找到了一種方法，可以在謂詞中傳遞一個函式，并且主要的遞回檢查在函式中，但它似乎不起作用。

錯誤基本上是“此呼叫的先決條件可能不成立”。
這是代碼：

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.

所有建設性的想法和 dafny 技巧都將被仔細閱讀。

謝謝。

uj5u.com熱心網友回復：

您的代碼有幾個問題。

(1)TreeADT上課的目的是什么？在 Dafny 中，類通常用于表示可變物件，但您的類沒有欄位或 mutator 方法，并且您使用 adatatype來保存資料，因此您可以完全擺脫類。

(2) 你的定義isBST是錯誤的。下面是一個例子：

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

這棵樹不是二叉搜索樹，因為 7 大于 5 但 7 在 5 的左子樹中。但是您的定義允許這棵樹。

(3) 你遇到的具體問題是 Dafny 無法證明變數tinMain是二叉搜索樹。我看到你有insert注釋掉的后置條件。為什么？您將需要該后置條件。

我也不確定“在謂詞中傳遞函式”是什么意思。您有一個無用（雖然無害）的包裝謂詞isBST。在 Dafny 中，這個詞predicate只不過是function回傳型別為的 a 的縮寫bool。

uj5u.com熱心網友回復：

添加幾個斷言陳述句后，您可以看到 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方法前置條件是輸入是有效的二叉搜索樹，后置條件是輸出是有效的二叉樹。因此，例如總是在樹下回傳的插入方法是有效的實作。

Dafny 謂詞 isBinarySearchTree

現在不難看出為什么當 temp 總是時treeMax或treeMin不會保持Tree(Tree(Nil, 1, Nil), 3, Tree(Nil, 5, Nil))。

回顧更大的問題是.輸入樹和輸出樹之間沒有鏈接ensures。

轉載請註明出處，本文鏈接：https://www.uj5u.com/yidong/356401.html

標籤：递归二叉搜索树谓词达夫尼

上一篇：撰寫遞回函式時，何時將“count”作為引數從一個遞回呼叫傳遞到另一個與定義“count =遞回函式”？

下一篇：DyalogAPL-河內塔-無法正常回圈