 Stack invariant

A property of the evaluation stack at a specified program point. For expression compilation, a useful contract is that generated code transforms any incoming stack $\sigma$ into $\sigma ,v$, leaving all pre-existing values unchanged. For a statement, a useful contract is preservation of $\sigma$.