Dafnyはスワップを使用して挿入ソートを検証します

Question

私はdafnyを使用して隣接する要素を「スワップ」して挿入のソートを検証する方法を研究していますが、whileループのために妥当な不変式を見つけることができません。 ここにリンクがあります：http://rise4fun.com/Dafny/wmYME

Answer 1

ここにいくつかの問題があります。

temp変数が決して更新されないため、最初に内部ループが正しくありません。 tempを削除し、代わりにループ条件down >= 0 && a[down+1] < a[down]を使用することをお勧めします。

第2に、インナーループインバリアントが形成されていない（インデックスが範囲外で、前提条件違反がsortedである）いくつかの問題があります。しかし、これらを修正するのではなく、内側ループ不変量を両方ともスローして、もう一度試してみることをお勧めします。

インサートソートの内側ループの優先不変量は、「a[0..up+1]はおそらくdown + 1にソートされています」です。これは、

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

と確認できます。