Runtime Assertion Checking for Old Expressions

[DavePearce]

(see also Whiley/WhileyCompiler#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 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

1. 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.
2. How the design of JML accommodates both runtime assertion checking and formal verification
3. A Runtime Assertion Checker for the Java Modeling Language (JML). "The runtime assertion checker handles old expressions by evaluating them in the pre-state inside the precondition check method and caching the results in private fields"
4. Prototyping a tool environment for run-time assertion checking in JML with communication histories
5. Temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties
6. An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs
7. Combining Monitoring with Run-Time Assertion Checking
8. OpenJML: JML for Java 7 by Extending OpenJDK
9. Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML
10. A Lesson on Runtime Assertion Checking with Frama-C
11. Runtime Assertion Checking and Static Verification: Collaborative Partners
12. Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups
13. Client-aware checking and information hiding in interface specifications with JML/ajmlc
14. Verified Runtime Assertion Checking for Memory Properties
15. The e-ACSL perspective on runtime assertion checking