Two-level semantics and code generation

compile-time correctness data flow analysis Kripke-like relations loop recursion run-time semantics of PASCAL-like languages two-level denotational metalanguage

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Review text

We present a two-level denotational metalanguage that is suitable for defining the semantics of PASCAL-like languages. The two levels allow for an explicit distinction between computations taking place at compile-time and computations taking place at run-time. While this distinction is perhaps not absolutely necessary for describing the input-output semantics of programming languages, it is necessary when issues like data flow analysis and code generation are considered. For an example stack- machine we show how to generate code for the run-time computations and still perform the compile-time computations. Based on an example it is argued that compiler-tricks like the use of activation records suggest how to cope with certain syntactic restrictions in the metalanguage. The correctness of the code generation is proved using Kripke-like relations and using a modified machine that can be made to loop when a certain level of recursion is encountered.

Recommendations

Cites work

Cited in

(21)

This page was built for publication: Two-level semantics and code generation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1095636)