Translation of Old() syntax

[DavePearce]

At this stage, there remain a lot of questions as to how we can safely translate occurrences of old(). Some can be done, such as this (Reference_Valid_1):

method swap(&int x_ptr, &int y_ptr)
ensures *x_ptr == old(*y_ptr)
ensures *y_ptr == old(*x_ptr):
    int tmp = *x_ptr
    *x_ptr = *y_ptr
    *y_ptr = tmp

But others cannot.