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.
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):But others cannot.