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;