我正试图在 dafny 中弄清楚一些事情。
给定 2 个数组 a 和 b，我的断言、不变量、后置条件等形式为：
multiset(a[..]) == multiset(b[..]);
失败但
multiset(a[..a.Length]) == multiset(b[..b.Length])
成功了。
我对此感到非常困惑，因为我认为 a[..] 和 a[..a.Length] 将是完全相同的东西。不过，我发现了一些有趣的事情。如果我在方法的末尾添加：
assert a[..a.Length] == a[..];
assert b[..b.Length] == b[..];
然后我可以让涉及我的第一个示例的不变量、后置条件、断言起作用。
这表明 a[..] 和 a[..a.Length] 实际上是不同的。
有人能解释一下为什么会这样吗？这里发生了什么？
【问题讨论】：
你说得对，a[..] 和 [..a.Length]（就此而言，a[0..] 和 a[0..a.Length]）是一回事。但是，验证者可能对这些略有不同。这会有所不同，因为 Dafny 中缺乏（注意：技术词即将出现）可扩展性。
扩展性意味着，如果你知道两个事物具有相同的元素，那么它们就是同一个事物。在您的示例中，可扩展性意味着，如果您知道 a[..] 和 a[..a.Length] 具有相同的元素，那么 a[..] 和 a[..a.Length] 是相同的。
Dafny 中缺乏可扩展性意味着验证者有时知道两个事物具有相同的元素，但仍不能得出两个事物相同的结论。当这两个东西被传递给一个函数时，这往往是显而易见的。在您的示例中，该函数是 multiset(...)，它将序列转换为多重集。
虽然 Dafny 不自动支持可扩展性，但它确实提供了一种简单的技术来“提醒”验证者有关可扩展性的信息。该技术是assert 两件事之间的平等。特别是当你为两个序列A和B写assert A == B;时，那么验证者会首先证明A和B有相同的元素，然后它会得出A实际上等于B的结论。换句话说，当明确要求验证者验证两个序列值表达式（如A 和B）的相等性时，它相反只是证明它们在元素方面相等，之后它的结论是A == B。
因此，您的上述补救措施是完全正确的做法。当你asserta[..a.Length] 和a[..] 相等时，验证者证明它们具有相同的元素。之后，它“记住”这也意味着a[..a.Length] 和a[..] 相等。一旦意识到这两个序列相同，它也立即知道它们的功能，如multiset(a[..a.Length])和multiset(a[..])，是相同的。
更一般地说，外延性不仅与序列有关，还与集合、多重集和映射有关。因此，如果您正在使用这些集合类型中的任何一种，您可能需要编写关于序列相等、集合相等等的断言，以“提醒”验证者有关可扩展性的信息。
更一般地说，有很多事情是真实的，验证者不会立即验证。要了解可能缺少的内容，常用技术是自己开始分解证明义务，就像您在 assert 声明中所做的那样。通过将更复杂的证明义务分解为更简单的义务（通常使用assert 语句或calc 语句完成），您实质上向验证者提供了有关如何证明更复杂事物的提示。
【讨论】：