Proving the Correctness of the Static Link Technique Using Evolving
Algebras
M. Mohnen
The {\em static link technique\/} is used for the stack-based
implementation of imperative programming languages which admit
nested recursive procedure declarations. It was suggested
in 1960 by Dijkstra as an extension of the stack technique
for the evaluation of expressions. Its basic idea is to
access global variables by tracing a static link chain to
lower stack elements. {\em Evolving algebras\/} are a new
method for the definition of operational semantics of abstract
machines. Based on an appropriate stack machine, defined as an
evolving algebra, and a functional description of a compiler
for a sample language, we will give a complete proof of this
technique. Especially, we will transform the evolving algebra
for the stack machine into a more abstract one, i.e., into
a new machine which is closer to the denotational semantics
of the sample language.