断言和设置基数

• 为什么下面的断言会失败？
• 另外，如果我取消评论，为什么所有断言都有效ASSERT 0（第 22 行）？

function CountFactors(i:nat): nat
  requires i >= 1;
{
  var a := set b | 1 <= b <= i && i % b == 0;
  |a|
}
function CountFactorsSet(i:nat): set<nat>
  requires i >= 1;
{
  var a := set b | 1 <= b <= i && i % b == 0;
  a
}
method CountFactorsMethod(i:nat) returns (a: set<nat>)
  requires i >= 1;
{
  a := set b | 1 <= b <= i && i % b == 0;
}
method Main()
{
  var r:= CountFactorsMethod(2);
  print(r);
  // assert CountFactorsSet(2) == {1, 2}; // ASSERT 0
  assert CountFactors(2) == 2; // ASSERT 1
}

这里是链接到代码 https://rise4fun.com/Dafny/Bp3j。我正在使用达夫尼 2.3.0.10506

在 Dafny 中使用集合（或映射或序列）时，这是一个非常常见的问题。这个问题归结为所谓的集合的“外延相等”。

在数学中，如果两个集合具有相同的元素，则它们相等。也就是说，（用伪 Dafny 语法）：

A == B   <==>   (forall x :: x in A <==> x in B)

这为在两步中证明集合相等提供了非常强大的推理原理。取任意元素A并显示它在B，然后取任意元素B并显示它在A.

不幸的是，从自动推理的角度来看，这是一项相当昂贵的任务。如果达夫尼试图通过这条规则证明每一个集合都等于它能想到的所有其他集合，那就太慢了。

相反，达夫尼采用以下经验法则：

我，达夫尼，不会尝试通过外延性证明两个集合相等，除非你在程序中明确要求我断言它们相等。

这通过限制 Dafny 考虑证明彼此相等的集合数量来控制验证性能。

所以，当你assert CountFactorsSet(2) == {1, 2};你允许达夫尼对这个集合进行外延推理CountFactorsSet(2)，事实证明这足以解决这个问题。

顺便说一句，在较大的程序中，如果你never重复一组理解两次。相反，始终将推导式包装在函数内，如下所示。

function CountFactorsSet(i:nat): set<nat>
  requires i >= 1;
{
  set b | 1 <= b <= i && i % b == 0
}
function CountFactors(i:nat): nat
  requires i >= 1;
{
  |CountFactorsSet(i)|
}

通过使用函数而不是直接使用推导式，您可以使 Dafny 的生活变得更加轻松，因为应用于相同参数的函数的两次出现是相等的，这变得“明显”，而对于 Dafny 来说，两个不同的语法出现并不“明显”相同的理解力是平等的。

事实证明，在你的例子中并不重要，但我只是想警告你，以防你计划更多地进行理解。