断言和设置基数

Question

为什么下面的断言会失败？
此外，如果我取消注释 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
}

这里是link to the code。我正在使用 Dafny 2.3.0.10506

Answer 1

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

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

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

这给出了一个非常强大的推理原理，用于证明两步集合相等。取A的任意一个元素，证明它在B中，然后取B的任意一个元素，证明它在A.

中

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

相反，Dafny 采用以下经验法则：

I, Dafny, will not try to prove two sets equal via extensionality unless you explicitly ask me to by asserting them equal in the program.

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

因此，当您 assert CountFactorsSet(2) == {1, 2}; 允许 Dafny 对集合 CountFactorsSet(2) 进行扩展推理时，事实证明这足以解决这个问题。

顺便说一句，在较大的程序中，如果您从不重复一个集合理解两次，您的运气会更好。相反，总是将理解包含在一个函数中，就像这样。

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 来说并不“明显”相同理解的两个不同句法出现是相等的。

在你的例子中结果并不重要，但我只是想我会警告你，以防你计划更多地使用理解。

断言和设置基数

Assertion and Set Cardinality

dafny