swap - 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]

结果文件验证。