JMLの評価\ old（式[Id]）

Question

\old(Expression[Id])という形式のJML式がどのように評価されているか、つまり\old(vector[value-1])式がある場合、\oldは「値」を参照するか、 vector[value-1]の値に設定します。前もって感謝します！

Answer 1

まあ、うまくいけば、あなたは他の場所であなたの質問への答えを見つけたが、それは最初のものです：

\old(vector[value-1])は\old(value)-1で古いベクトルの値です。