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] 

生成的文件將進行驗證。