Thumbnail
Access Restriction
Open

Author Heberle, Andreas ♦ Löwe, Welf
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Asm-based Specification ♦ Reusable Correct Compilation ♦ Programming Language Semantics ♦ Dynamic Programming Language Semantics ♦ Formal Specification ♦ Verified Transformation ♦ Correct Compiler ♦ Extensible Language Al ♦ Intermediate Language ♦ Object-oriented Verified Implementation ♦ Correct Compilation ♦ Operational Specification ♦ Language Semantics ♦ Introduction Abstract State Machine ♦ Asm Specification ♦ General Transformation ♦ Verified Construction ♦ Programming Language
Abstract . 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 ...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Publisher Date 1998-01-01