Stack invariant
= 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$.