問題タブ [dafny]

メソッドでやりたいことは、前の配列を上書きして、並べ替えられた数値で埋めることですが、dafny は、事後条件が保持されず、私の人生では理由を理解できないと言っています。ループに不変条件を追加する必要があると思いますが、ループに入る前にチェックされるため、有効な不変条件を配置する方法がわかりません。

私の以前の試みは a を再初期化することだけでしたが、dafny はメソッド内でそれを許可していないようです。

メソッドで、変更済みとしてマークされている配列を上書きするにはどうすればよいですか? または、Dafny で配列の長さを 1 だけ増やす方法はありますか?

このコードでわかるように。メソッドextendArrayByOneで配列の長さを1つ増やそうとしています。その後、メソッドconfirmAndCheckで、extendArrayByOneから返された新しい配列の最後に要素操作を追加しています。このコードをコンパイルできる公式コンパイラへのリンクは次のとおりです: https://rise4fun.com/Dafny/WtjA

そして、これがextendArrayByOneに関する私の以前の質問へのリンクです:

変更されたオブジェクトの変更節エラー

Dafnyで有限集合オブジェクトの要素を反復処理する最良の方法は何ですか? 動作するコードの例は楽しいでしょう。