Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Verifying an Open Compiler Using Multi-language Semantics
verfasst von : James T. Perconti, Amal Ahmed
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Existing verified compilers are proved correct under a closed-world assumption, i.e., that the compiler will only be used to compile
whole
programs. We present a new methodology for verifying correct compilation of program
components
, while formally allowing linking with target code of arbitrary provenance. To demonstrate our methodology, we present a two-pass type-preserving open compiler and prove that compilation preserves semantics. The central novelty of our approach is that we define a combined language that embeds the source, intermediate, and target languages and formalizes a semantics of interoperability between them, using boundaries in the style of Matthews and Findler. Compiler correctness is stated as contextual equivalence in the combined language.
Note to reader: We use
blue
,
red
, and
purple
to typeset terms in various languages. This paper will be difficult to follow unless read/printed in color.