Past exam of the computer science course of the University of Oxford / 2015 / Compilers / 2 / d

Use mathematical induction on the sequence of call and return events. The invariant concerns the static chain of the currently executing activation: every stack frame on that chain is the most recent surviving activation of the procedure it represents. It need not hold for the saved chain of an arbitrary suspended caller while a recursive callee is running.

Initially only main is active, so the claim holds. Suppose it holds just before a direct call to a procedure $R$, whose lexical parent is $P$. Without procedural parameters, visibility of $R$ means that its declaration lies in the current procedure or in a lexically enclosing procedure. Therefore the activation of $P$ needed for the call is on the caller's static chain. By the induction hypothesis, it is the newest surviving activation of $P$.

Create a new activation of $R$ whose static link points to this $P$ activation. The inherited chain is a suffix of the caller's chain, so its stack frames still represent the newest surviving activations of their procedures. Adding $R$ does not make any of those inherited activations out of date: $R$ cannot be its own lexical ancestor. The new $R$ activation itself is plainly the newest activation of $R$. This covers recursive calls too: an older activation of $R$ may survive on the dynamic chain, but is absent from the new activation's static chain.

On return, the callee and every call it made have finished. The caller's saved stack frame and static chain are restored. Any temporarily newer activation of a procedure represented on that chain has returned, so each restored activation is again the most recent surviving one. Thus return preserves the invariant as well.

The claim holds for the executing procedure's static chain throughout every execution using direct calls under lexical scope. Equivalently, writing $P_F$ for the procedure represented by a stack frame $F$,