如何证明Dafny中BST删除操作后仍为二叉搜索树？

问题背景 #

需要验证Dafny实现的二叉搜索树（BST）删除函数执行后，返回的树仍符合BST特性。当前函数逻辑框架正确，但递归执行后的BST约束无法自动保证，已引入Size函数用于递归终止证明，以下是具体证明思路：

一、先修正基础定义与函数约束 #

1. 调整辅助函数命名与逻辑一致性
   当前greater/lesser函数的命名和实际逻辑匹配度不高（比如greater(tree, max)实际是判断树中所有节点都小于max），建议重命名为allLessThan(tree, val)和allGreaterThan(tree, val)，避免逻辑混淆，也便于后续证明时的语义理解。

2. 强化删除函数的后置条件
   原Deletion函数的后置条件仅覆盖了左子树为空的特殊情况，需要直接断言核心目标：

   ensures isBinarySearchTree(Deletion(tree, v))
   

   这是证明的核心结论，所有分情况讨论最终都要指向这个断言。

二、分递归场景逐一证明 #

利用Dafny的归纳证明特性（结合decreases Size(tree)保证递归终止），针对删除函数的每个分支逐一验证：

1. 空树分支（tree == Nil） #

直接返回Nil，isBinarySearchTree(Nil)天然为真，无需额外证明。

2. 删除值小于当前节点值（v < x） #

递归调用Deletion(ltree, v)得到新左子树new_ltree：

• 由递归前置条件，原左子树ltree是BST；结合归纳假设（因为Size(new_ltree) < Size(tree)），递归返回的new_ltree仍为BST。
• 原右子树rtree满足allGreaterThan(rtree, x)（原树是BST的约束），且删除左子树中的节点不会引入大于等于x的节点，因此new_ltree仍满足allLessThan(new_ltree, x)。
• 组合后的Node(new_ltree, x, rtree)满足BST的所有定义：左右子树都是BST，左子树所有节点小于x，右子树所有节点大于x。

3. 删除值大于当前节点值（x < v） #

与场景2完全对称，递归删除右子树后，新右子树new_rtree仍为BST，且满足allGreaterThan(new_rtree, x)，原左子树保持allLessThan(ltree, x)，组合后的树符合BST约束。

4. 当前节点为待删除节点（x == v） #

分两种子情况处理：

子情况4.1：左子树为空（ltree == Nil）

直接返回右子树rtree，原树是BST则rtree必然是BST，满足要求。

子情况4.2：左子树非空

当前逻辑是用左子树的根节点v2替换当前节点，然后递归删除Node(rtree2, x, rtree)中的v：

• 首先证明Node(rtree2, x, rtree)是BST：原左子树的右子树rtree2满足allGreaterThan(rtree2, v2)且allLessThan(rtree2, x)（原树BST的约束），原右子树rtree满足allGreaterThan(rtree, x)，因此该组合树符合BST定义。
• 结合归纳假设，递归删除后的new_rtree仍为BST，且new_rtree中所有节点都大于v2（因为原rtree2大于v2，原rtree大于x而x大于v2，删除v不破坏这个约束）。
• 左子树的左分支ltree2是原BST的一部分，本身就是BST且所有节点小于v2，因此最终组合的Node(ltree2, v2, new_rtree)满足BST的所有条件。

三、补充辅助函数的性质引理 #

为了让Dafny自动验证上述逻辑，需要补充辅助函数的关键性质：

• 引理1：如果allLessThan(tree, val)成立，删除tree中的任意节点后，新树仍满足allLessThan(new_tree, val)。
• 引理2：如果allGreaterThan(tree, val)成立，删除tree中的任意节点后，新树仍满足allGreaterThan(new_tree, val)。
• 引理3：若左子树是BST且所有节点小于val，右子树是BST且所有节点大于val，则Node(left, val, right)是BST。

这些引理可以单独用Dafny的lemma语法定义并证明，作为删除函数证明的前置依赖。

修正后的核心代码示例 #

datatype Tree = Nil | Node(ltree: Tree, v: int, rtree: Tree)

function Size(tree: Tree): nat
  decreases tree
{
  match tree
  case Nil => 0
  case Node(l, _, r) => 1 + Size(l) + Size(r)
}

function isBinarySearchTree(tree: Tree) : bool
  decreases tree
{
  match tree
  case Nil => true
  case Node(ltree,v,rtree) =>
    isBinarySearchTree(ltree) && isBinarySearchTree(rtree)
    && allLessThan(rtree, v) && allGreaterThan(ltree, v)
}

function allGreaterThan(tree: Tree, bound: int) : bool
  decreases tree
{
  match tree
  case Nil => true
  case Node(ltree,v,rtree) => (v > bound) && allGreaterThan(ltree, bound) && allGreaterThan(rtree, bound)
}

function allLessThan(tree:Tree, bound: int) : bool
  decreases tree
{
  match tree
  case Nil => true
  case Node(ltree,v,rtree) => (v < bound) && allLessThan(ltree, bound) && allLessThan(rtree, bound)
}

function Deletion(tree:Tree, v:int): Tree
  requires isBinarySearchTree(tree)
  decreases Size(tree)
  ensures isBinarySearchTree(Deletion(tree, v))
{
  match tree
  case Nil => Nil
  case Node(ltree, x, rtree) =>
    if (v < x) then Node(Deletion(ltree, v), x, rtree)
    else if (x < v) then Node(ltree, x, Deletion(rtree, v))
    else match ltree {
           case Nil => rtree
           case Node(ltree2, v2, rtree2) =>
             Node(ltree2, v2, Deletion(Node(rtree2, x, rtree), v))
         }
}

内容的提问来源于stack exchange，提问作者1bitcode