我对任何可验证的 CountLessThan 编写方式持开放态度。这是我所拥有的：
function SetLessThan(numbers: set<int>, threshold: int): set<int>
{
set i | i in numbers && i < threshold
}
method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
ensures count == |SetLessThan(numbers, threshold)|
{
count := 0;
var shrink := numbers;
var grow := {};
while |shrink | > 0
decreases shrink
invariant shrink + grow == numbers
invariant count == |SetLessThan(grow, threshold)|
{
var i: int :| i in shrink;
shrink := shrink - {i};
grow := grow + {i};
if i < threshold {
count := count + 1;
}
}
}
method Main()
{
var s: set<int> := {1, 2, 3, 4, 5};
var c: int := CountLessThan(s, 4);
print c;
// assert c == 3;
}
这是定义排序集、排序映射、范围集的一小步。
您面前有一个经典的验证调试练习:)
验证调试的基本方法是添加
assert语句来缩小问题所在的范围。我写下了理想化调试会话的完整记录。如果您只想要工作代码，请随意跳到最后。
您帖子中的代码报告了循环不变量的以下错误：
这意味着 Dafny 无法在循环底部重新建立不变量。让我们将其转换为断言。
我们实际上并没有做任何事情，但请注意，不再报告不变量的错误，因此总共只有一个错误。达夫尼说的是“如果你能证明这个断言，那么其余的代码也会验证”。
现在我们开始将断言向后移动到循环中。将其移至单侧 if 语句的最简单方法是人为地引入一个空
else分支，然后在两侧复制断言。请注意，最底部的错误
assert消失了。我们有两个错误，但如果我们能修复这些错误，我们就完成了。我们正在取得进展。在第一个分支中，我们现在将
assert作业向后移动。为此，我们将出现的替换count为：count + 1assert请注意，仍然只有两个错误。
现在我们需要将断言从
if. 最简单的方法是使用 -if表达式。Dafny 显示仍然显示两个分支的单独错误，但它们现在再次成为一个
assert语句的一部分，取得了更多进展。接下来我们将作业移回
grow。我们在断言中替换grow + {i}为。grow我们已经成功地再次转移了错误。
我们可以继续回顾这个
shrink作业，但因为它与这个断言无关，所以没关系，所以让我们留在这里。至此，我们已经消除了验证问题中的所有“命令性的东西”，只剩下“逻辑性的东西”需要担心了。我们来证明一下这个断言。
首先，我们可以重写断言以将其
==从if-then-else. 将其放在assert上一个之上。这是我们现在唯一的错误，所以我们仍在进步。如果我们能证明这一点，达夫尼将证明其余的事情。
count我们也可以找出 的发生。将此断言放在前一个断言之上。我们将用一个
calc计算块来证明这一点。将此块放在前一个断言之上。我们有一个关于 的循环不变式
count，所以让我们将其代入。仍然只有一个错误，因此达夫尼同意我们计算的第一步。
为了填补第二行和第三行之间的空白，我们需要连接集合
SetLessThan(grow + {i}, threshold)和SetLessThan(grow, threshold)。它们是如何连接的？那么如果i < threshold前者是后者的加i，否则它们就相等。这么说吧。请注意，顶部的断言没有错误！所以达夫尼喜欢我们设定的相等性，但仍然无法证明基数事实。
让我们尝试通过将基数运算符拉到加号之外来填补第二行和第三行之间的空白。
啊哈！错误移动了。现在最后一行和倒数第二行相等，但中间两行不同。是什么赋予了？
嗯，并集的基数并不总是基数之和。仅当它们不相交时才是正确的。这些集合是不相交的吗？是的！为什么？因为我们退出
i了收缩，并且grow和shrink是脱节的。但达夫尼无法判断，因为我们需要另一个循环不变量。在 Dafny 中，
A !! BmeansA和B是脱节的。我们添加这个循环不变量：
所有的错误都消失了！！！呜呜。我们庆祝。
现在我们清理干净。我们添加了大量不必要的断言，现在我们可以删除这些断言并找出真正重要的内容。只需尝试删除一些内容并查看仍然可以验证的内容即可。
事实证明，唯一重要的是循环不变式和 1
assert。这是最后的循环