= Solution
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.
\b[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$,
$$
\boxed{F\in\mathrm{staticChain}_{\mathrm{executing}}\ \Longrightarrow\ F=\mathrm{newestSurviving}(P_F).}
$$
Back to article page
