2002 | OriginalPaper | Buchkapitel
Refinement Algebra for Formal Bytecode Generation
verfasst von : Adolfo Duran, Ana Cavalcanti, Augusto Sampaio
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
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
In this paper we propose an strategy for the design of compilers correct by construction for object-oriented languages. The process is formalized within a single and uniform semantic framework of an object-oriented language based on a subset of sequential Java and its algebraic laws. The strategy is to reduce an arbitrary source program to a particular normal form which describes the behavior of the target machine. This behavior is defined by an interpreter written in the same language. From the interpreter we can capture the sequence of generated bytecodes of the target machine. The normal form reduction is formalized as algebraic transformations where the central notion is refinement of programs.