I have to write a little BST (binary search tree) class in Dafny.
I begin with Dafny then write a class and an insert method was the easiest part.

I tried multiple time to write a recursive predicate which can check if the tree passed as argument is a BST (without balancing condition, a simple binary tree following the rule left.value < node.value && right.value > node.value).

I found in another StackOverflow post a way to do it passing a function in a predicate and the main recursives check are in the function but it doesn't seem to work.

The error is basically 'A pre-condition for this call might not hold'.
Here is the code:

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

I also tried to do it entirely in the predicate but the recursive check seems to doesn't work anyway.

Any idea to get recursion check instead of loop check in a predicate?

Thanks for reading.

Edit:
Following James's answer i modified my code

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

But same problem occurs in requires and ensures statement, I now check if all value at left side are lesser and all at right side are greater but this error occurs again

A postcondition might not hold on this return path.

And if I comment out the ensures statement I get the following error:

A precondition for this call might not hold.

All constructives ideas and dafny tips will be read with attention.

Thanks.

CodePudding user response：

There are several issues with your code.

(1) What is the purpose of the TreeADT class? In Dafny, classes are usually used to represent mutable objects, but your class has no fields or mutator methods, and you use a datatype to hold the data, so you can just get rid of the class altogether.

(2) Your definition of isBST is wrong. Here is an example:

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

This tree is not a binary search tree because 7 is greater than 5 but 7 is in the left subtree of 5. But your definition allows this tree.

(3) The concrete problem you are running into is that Dafny cannot prove that the variable t in Main is a binary search tree. I see you have that postcondition of insert commented out. Why? You will need that postcondition.

I'm also not sure what you meant by "passing a function in a predicate". You have a useless (though harmless) wrapper predicate isBST. In Dafny, the word predicate is nothing but an abbreviation for a function whose return type is bool.

CodePudding user response：

After adding few assert statements you can see what dafny is unable to verify.

   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 is unable to verify added assert holds. Way to think about why dafny is unable to verify is it looks abstractly all method with given pre and post conditions forgetting implementation. insert method precondition is input is valid binary search tree and postcondition is output is valid binary tree. So insert method which always return below tree for example is valid implementation.

Now it is not hard to see why treeMax or treeMin will not hold when temp is always Tree(Tree(Nil, 1, Nil), 3, Tree(Nil, 5, Nil)).

Looking back bigger issue is there is no link between input tree and output tree provided by ensures.