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)后置条件。

它可以推断元素集的基数小于或等于大小函数，但不能推断它相等。我试图断言这两个树不变的Valid谓词中元素的唯一性，但它仍然不能证明函数的正确性。你知道我该怎么做吗？

Answer 1

您可以通过添加如下内联断言来证明此post条件：

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)，即使它们不是那么明显。