dafnyの配列を上書きする

Question

メソッド内の配列を上書きしようとしています。コンパイラは私にエラー "エラー：割り当てのLHSは可変変数を示さなければなりません"を与えています。

私は自分自身を見つめて何かを見失っていますか、なぜDafnyはこれを許可していませんか？

Answer 1

Dafnyでは、メソッドパラメータを割り当てることができません。内部的に値を更新する必要がある場合は、ローカル変数を使用できます。例えば

、

var a' := new int[0]; 

あなたがこの新しい配列は、発信者が利用できるようにしたい場合は、それを返す必要があります。

return a';  

つまり、インプレースソート方法を作成しようとしている場合は、これを行う必要はありません。ただaを変更してください。

a[0] := 0; 
// ...