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] 

生成的文件将进行验证。