Dafny 使用交换验证插入排序

Question

我正在研究如何使用 dafny 来验证使用“交换”相邻元素的插入排序，但我找不到 while 循环的合理不变量，谁能帮我解决它？ 这是链接：http://rise4fun.com/Dafny/wmYME

Answer 1

这里有一些问题。

首先，您的内部循环不正确，因为 temp 变量永远不会更新。我建议删除temp 并改用循环条件down >= 0 && a[down+1] < a[down]。

其次，内部循环不变量格式不正确有几个问题（索引超出范围，违反sorted 的前提条件）。但是，我建议不要修复这些，而是​​丢弃两个内部循环不变量并重试。

对于插入排序的内部循环，我首选的不变量是“a[0..up+1] 已排序，但可能在 down + 1 处除外”。您可以将其声明为

invariant forall j,k | 0 <= j < k < up+1 && k != down+1 :: a[j]<=a[k]

生成的文件验证。