在 Dafny 中证明二叉搜索树的大小

Question

我试图证明在 Dafny 中实现二叉搜索树的正确性，但我正在努力证明计算出的大小对应于元素集的大小。

到目前为止，我已经编写了以下代码：

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 未能证明 size 函数，特别是 ensures |elems(treeSet)| == size(treeSet) 后置条件。

可以推断出元素集合的基数小于等于size函数，但不能推断出相等。我试图断言 Valid 谓词中元素的唯一性树不变量，但它仍然无法证明函数的正确性。知道我该如何完成这项工作吗？

Answer 1

您可以通过添加这样的内联断言来证明这个后置条件：

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

其他注意事项：

• 我认为您的 descendants 函数有些奇怪：它总是返回空集！

• 在Valid 中，您不需要子句treeSet != left 或treeSet != right，根据数据类型声明，这些对Dafny 来说是“显而易见的”。您可能也不需要treeSet !in descendants(left) 或treeSet !in descendants(right)，即使它们并不那么明显。