On ASM-Based Specification of Programming Language Semantics and Reusable Correct Compilations.
Andreas Heberle, Welf Löwe · 1998
. We define general transformations on ASM specifications of programming language semantics. These transformations preserve the semantics of the programming language and can thus be used for the definition of correct compilations. Additionally, we define an extensible language AL for the specification of dynamic programming language semantics and describe how this allows reuse of verified transformations. Together with a library of object-oriented verified implementations this leads to a framework for the construction of correct compilers based on the formal specification of source and intermediate language. 1 Introduction Abstract state machines are well suited for the operational specification of dynamic programming language semantics. They were used for the specification of C ([GH93]), C++ ([Wal94]) and Java ([BS98]) or with Montages for the specification of Oberon ([KP97a])and SQL ([DiF97]). For the verified construction of compilers the formal specification of source and target ...