Dafny 使用交换验证插入排序

Dafny verifies insertion sort using swap

我正在研究如何使用 dafny 来验证使用 "swap" 相邻元素的插入排序,但我找不到 while 循环的合理不变量,谁能帮我解决这个问题? 这是 link:http://rise4fun.com/Dafny/wmYME

这里有一些问题。

首先,您的内部循环不正确,因为 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]

生成的文件验证。