Improved Syntax for Framing

[DavePearce]

(see also #82)

I need to update this RFC: https://github.com/Whiley/RFCs/blob/master/text/0067-old-values.md

I think we need to separate out two things:

1. The value of a variable in the pre-state
2. The value of the heap in the pre-state

Currently, the proposal allows an arbitrary "old expression" form '*e' with an eye to eventually allowing'e'`. I think there are some ambiguities here though. What is the meaning of these forms?

• '*v' --- value in _old_ heap identified by _current_ value ofv`
• '*'v --- value in old heap identified by old value of v
• '**v --- value in old heap identified by value in old or new heap identified by current value of v.

This is not making sense. We want two expression forms:

• #e the value in the old heap identified by e. This is like *e but for the old heap.
• 'v the old value of variable v.

Now, we can disambiguate the last case above as either ##v or #*v.

What about method calls? Do we need a syntax like m#() or similar?

[DavePearce]

At this stage, it seems like going with old(e) for now makes the most sense.