Thumbnail
Access Restriction
Open

Author Mohnen, Markus
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Compiler Correctness Proof ♦ Static Link Technique ♦ Imperative Programming Language ♦ Sample Language ♦ Nested Recursive Procedure Declaration ♦ New Method ♦ Well-known Static Link Technique ♦ Appropriate Stack Machine ♦ Easy Task ♦ Stack-based Implementation ♦ Static Link Chain ♦ Stack Element ♦ Way Variable ♦ Operational Semantics ♦ Functional Description ♦ First Case ♦ Abstract Machine ♦ Local Variable ♦ Complete Proof ♦ Nested Procedure Declaration ♦ Basic Idea
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. Introduction The assignment of values to variables is at the basis of imperative programming languages. Consequently, the way variables are accessed is crucial for the implementation of such languages. This is an easy task as long as there is either no recursion (as with FORTRAN77) or no nested procedure declarations (as with C) in the language. In the first case, each variable in the program gets a stat...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study