如何帮助Dafny验证器证明非负整数集合的基数等于n？

显然，小于n的非负整数集合的基数为n，但Dafny无法直接证明以下代码的后置条件：

method FirstNonnegatives(n: nat) returns (s: set<nat>)
    ensures |s| == n
{
    s := set k | 0 <= k < n;
}

可通过以下几种修改帮助验证器完成证明：

• 添加辅助断言明确集合范围：在集合赋值后添加断言，清晰定义集合元素的归属条件，帮助验证器关联元素范围与基数的关系：

  method FirstNonnegatives(n: nat) returns (s: set<nat>)
      ensures |s| == n
  {
      s := set k | 0 <= k < n;
      assert forall k: nat :: k in s <==> 0 <= k < n;
      assert |s| == n;
  }
  

• 改用构造性集合定义：用循环逐个添加元素的方式替代集合推导式，通过循环不变式直接维护集合大小，让验证器能逐步跟踪基数变化：

  method FirstNonnegatives(n: nat) returns (s: set<nat>)
      ensures |s| == n
  {
      s := {};
      var i := 0;
      while i < n
          invariant |s| == i
          invariant forall k: nat :: k in s <==> 0 <= k < i
      {
          s := s + {i};
          i := i + 1;
      }
  }
  

• 显式引用内置证明规则：通过断言直接指出区间集合的基数等于n，触发Dafny内置的相关引理完成证明：

  method FirstNonnegatives(n: nat) returns (s: set<nat>)
      ensures |s| == n
  {
      s := set k | 0 <= k < n;
      assert |set k | 0 <= k < n| == n;
  }
  

内容的提问来源于stack exchange，提问作者Frank Seidl