Dafnyコンテキスト変更句エラー

Question

私のDafnyプログラムの最後のエラーを取り除くのに本当に苦労しています。誰かが私を正しい方向に向けることができますか？ http://rise4fun.com/Dafny/2FPo

私はこのエラーを取得しています：割り当てはない外側のコンテキストの修正条項に

を配列要素を更新することが、私はかなり確信しているにもかかわらず、マージ方法（で修正四角形を追加しようとした。ここ コードですこれはすでに変更されていますが、これは単にマージメソッド呼び出しで同様のエラーを生成します）。

私は本当にこの1つを失っています。助けをありがとう

Answer 1

問題は、 "これを変更する"は、これらのフィールドが指すものの変更ではなくフィールドの変更を許可することです。メソッドがやっていた言い換えれば、それは適切であろう：

this.rectangles := new_rectangle_array; 

ではなく、それはやっていた場合：

は

this.rectangles[3] := new_rect; 

だから、あなたが持っている場所で、「これを変更し、」あなたの代わりに持っている必要があります"四角形を修正する"。

同様の理由で、Testには「modify c.rectangles」と注釈を付ける必要がありますが、「cを変更する」ではありません。

最後に、DafnyがTestを呼び出すことを納得させるために、Couvertureのコンストラクタに四角形のフィールドを制約する事後条件を与える必要があります。それ以外の場合、検証者はTestを呼び出すことができないと確信することはできません。検証者が知る限り、couvは、Mainが変更できないランダムな配列を含んでいる可能性があります。

フルコードについては、http://rise4fun.com/Dafny/Skrgを参照してください。