断言和集合基数答案

【问题标题】：Assertion and Set Cardinality断言和集合基数
【发布时间】：2020-11-21 17:08:53
【问题描述】：

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

【问题讨论】：

标签： dafny

【解决方案1】：

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

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

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

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

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

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

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

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

在你的例子中结果并不重要，但我只是想我会警告你，以防你打算更多地使用推导式。

【讨论】：