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 (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;