Dafny検証 - 事後条件で元のvarを参照してください

Question

私はDafnyで自分のコードを検証しようとしていますが、問題が発生しました： シーケンスを反復処理して変更するメソッドがあります。このメソッドは、シーケンス内の要素に従ってシーケンスを変更します。私はこのようなポスト条件を追加したいと思います： "シーケンスの要素がXなら何かが起こるはずです"。問題は、メソッドがセットを変更する（要素を追加するなど）、元のシーケンスの状態をチェックしたいということです。 Dafnyでそれを行うエレガントな方法はありますか？ （私が今考えている唯一の方法は、配列の元の状態をグローバル変数に保つことですが、それを行う正しい方法を探しています）。

コード例：コードで

method changeSeq(p: class1, s: seq<class1>) 
ensures |s| == 10 ==> p in s 
{ 
    if (|s| == 10){ 
     s := s + [p]; 
    } 
} 

、私たちはそれを変更した後、ポスト条件がSTATを元のスタットをチェックし、しないようにしたいです。

Answer 1

のような変数の古い値にはoldを使用できます。ここで

は一例です：Dafny Documentation 22.18. Old Expressions

OldExpression_ = "old" "(" Expression(allowLemma: true, allowLambda: true) ")"

からhttp://rise4fun.com/Dafny/fhQgD

古い表現は事後条件で使用されています。 old(e)は、現在のメソッドへの入力時に値式eを評価します。 古いは、o.fとa[i]のようなヒープの参照解除にのみ影響することに注意してください。特に、oldは、ローカル変数またはoutパラメータに対して返される値に影響しません。