old() Basics
The old() expression captures the value of a field or expression at method entry. It lets postconditions and proof-only assertions relate the state you started with to the state you return.
Restrictions
The old() expression is restricted to specific contexts where it makes semantic sense. This page explains where old() can and cannot appear, and why.
Common Patterns
This page presents practical patterns for using old() in real verification scenarios. These patterns appear frequently when proving properties about state-changing methods.