There are a number of questions around old(e) expressions and how they can be checked at runtime efficiently. At the moment, the Whiley interpreter clones the entire program state --- which is pretty inefficient. For example, in the JML Runtime Assertion Checker, they evaluate old(e) expressions on entry to a method and stash them for checking the postcondition. But, this is very problematic for a few reasons: firstly, how do we manage recursive properties involving old()? secondly, how do we handle quantified expressions, etc?
References
Past Expression: Encapsulating Pre-States at Post-Conditions by Means of AOP Proposes \past(e) to replace \old(e) in JML to address the issue that (in Java) \old(p) for some class variable p only returns its reference, and there is no way to do e.g. \old(*p) as we can in Whiley. Yes, we can do e.g. \old(p.f) for each field, but this breaks encapsulation. To address performance of runtime checking, they employ a difference heap.
(see also https://github.com/Whiley/WhileyCompiler/issues/1096)
There are a number of questions around
old(e)expressions and how they can be checked at runtime efficiently. At the moment, the Whiley interpreter clones the entire program state --- which is pretty inefficient. For example, in the JML Runtime Assertion Checker, they evaluateold(e)expressions on entry to a method and stash them for checking the postcondition. But, this is very problematic for a few reasons: firstly, how do we manage recursive properties involvingold()? secondly, how do we handle quantified expressions, etc?References
\past(e)to replace\old(e)in JML to address the issue that (in Java)\old(p)for some class variableponly returns its reference, and there is no way to do e.g.\old(*p)as we can in Whiley. Yes, we can do e.g.\old(p.f)for each field, but this breaks encapsulation. To address performance of runtime checking, they employ a difference heap.