Old
Inside an ensure Post-Condition block, the old operator can be used to refer to the original value a parameter, Field or Property had at the beginning of the method. This can be useful for checking the validity of the result compared to the previous state. Note that for heap-based Reference Types (except Strings such as Classes, which receive special handling), the old operator only captures the old reference, but not the old state of the object it contains.
method MyClass.IncrementCount(aBy: Int32);
require
aBy > 0;
begin
fCount := fCount + aBy
ensure
fCount - aBy = old fCount;
end;