dafny - Dafny：不检查多个谓词

Question

目前，我尝试在 Dafny Repo 中编写现有二叉树的平衡版本（AVL-Tree）。我可以验证这棵平衡树仍然是有效的二叉树。

为了验证它是否也满足 AVL 树的要求，我创建了两个额外的谓词。这些谓词验证子树的高度是否有效以及节点及其子树是否平衡。

由于高度有效性检查需要有效的二叉树，而平衡检查需要有效的高度计算，因此谓词相互依赖：

  predicate Heigth_Valid() 
    reads this, Repr 
  {
    Valid() &&
    (..)
  }

  predicate Balanced() 
    reads this, Repr
  {
    Valid() &&
    Heigth_Valid() &&
    (..)
  }

  predicate Valid()
    reads this, Repr
  {
    (..)
  }

因此，可以将验证拆分为不同的方法，因为有些方法可能只提供有效的二叉树，而其他方法则重新计算高度或平衡树。

树平衡的验证是成功的，但是当我尝试用反例检查验证并更改代码以生成不平衡树时，Dafny 在 IDE 中没有显示错误。Dafny 是否有可能忽略某些谓词？

标签： dafny