A COMPILER CORRECTNESS PROOF FOR THE STATIC LINK TECHNIQUE BY MEANS OF EVOLVING ALGEBRAS

Article type: Research Article

Authors: Mohnen, Markus

Affiliations: RWTH Aachen, Lehrstuhl für Informatik II, Ahornstraße 55, 52056 Aachen, Germany e-mail: mohnen@informatik.rwth-aachen.de

Abstract: The well-known static link technique is used for stack-based implementations of imperative programming languages which admit nested recursive procedure declarations. Its basic idea is to access non-local variables by tracing a static link chain to lower stack elements. Evolving algebras are a new method for defining 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 give a complete proof of correctness for this technique using the method of refinement.

DOI: 10.3233/FI-1997-29303

Journal: Fundamenta Informaticae, vol. 29, no. 3, pp. 257-303, 1997