Implement old() Syntax

[DavePearce]

This is a little controversial, since I haven't figure out all the details yet! But, what the heck. Let's get a preliminary implementation for \old() syntax into the compiler.

[DavePearce]

References

1. Past Expression: Encapsulating Pre-States at Post-Conditions by Means of AOP.
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)
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

[DavePearce]

One problem which needs to be resolved is runtime checking of old(e) expressions. The obvious solution is to save the entire machine state on entry to a method, but that's kind of ridiculous. The solution used in JML was to execute old(e) expressions at the beginning of a method, and save their results for use in the postcondition. One problem with this arises from quantifiers and, in particular, old(e) expressions which contain quantified variables.

Part of the issue here is that, in the current design of the interpreter, its quite difficult to snapshot the machine state since references are actually implemented using JVM Objects.

[DavePearce]

My current solution to the issue of handling old(e) expressions is actually to save the entire state on entry to a method. This is obviously costly, but provides a simple semantic. The problem I have is that evaluating old(e) in the prestate on entry to a method is extremely difficult to manage correctly. For example, if we have a recursive variant ... how to do we determine the set of locations to which it might refer? We can't.