Proving size of Binary Search Tree in Dafny

user_14720794 0
Viewed 206

I am trying to prove the correctness of a binary search tree implementation in Dafny, but I am struggling to prove that the computed size corresponds to the size of the elements set.

So far I have written the following code:

datatype TreeSet =
   Leaf
 | Node(left: TreeSet, data: int, right: TreeSet)

predicate Valid(treeSet: TreeSet) {
    match treeSet
        case Leaf => true
        case Node(left, data, right) => Valid(left) && Valid(right)
            && treeSet != left && treeSet != right
            && (forall elem :: elem in elems(left) ==> elem < data)
            && (forall elem :: elem in elems(right) ==> elem > data)
            && treeSet !in descendants(left)
            && treeSet !in descendants(right)
}

function descendants(treeSet: TreeSet) : set<TreeSet> {
    match treeSet {
        case Leaf => {}
        case Node(left, _, right) => descendants(left) + descendants(right)
    }
}

function size(treeSet: TreeSet): nat
requires Valid(treeSet)
ensures |elems(treeSet)| == size(treeSet)
{
  match treeSet
    case Leaf => 0
    case Node(left,_,right) =>
      size(left) + 1 + size(right)
}

function elems(treeSet: TreeSet): set<int>
{
    match treeSet
        case Leaf => {}
        case Node(left, data, right) => elems(left) + {data} + elems(right)
}

Dafny is failing to prove the size function, specifically the ensures |elems(treeSet)| == size(treeSet) postcondition.

It can infer that the cardinality of the element set is lesser than or equal to the size function, but not that it is equal. I tried to assert both the tree invariant the uniqueness of elements in the Valid predicate, but it still cannot prove the correctness of the function. Any idea of how I could make this work?

dafny
1 Answers

You can prove this post condition by adding an inline assertion like this:

function size(treeSet: TreeSet): nat
requires Valid(treeSet)
ensures |elems(treeSet)| == size(treeSet)
{
  match treeSet
    case Leaf => 0
    case Node(left,x,right) =>
      assert forall elem :: !(elem in elems(left) && elem in elems(right));  // NEW
      size(left) + 1 + size(right)
}

Couple other notes:

  • I think something is weird with your descendants function: it always returns the empty set!

  • In Valid, you don't need the clauses treeSet != left or treeSet != right, those are "obvious" to Dafny based on the datatype declaration. You probably also don't need treeSet !in descendants(left) or treeSet !in descendants(right) even though they are not so obvious.

user_4382670
Related