java - \old(Expression[Id]) の JML 評価

Question

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

Answer 1

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

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