Duran, Adolfo and Sampaio, Ana and Cavalcanti, Augusto (2002) Refinement Algebra for Formal Bytecode Generation. In: Formal Methods and Software Engineering: 4th International Conference on Formal Engineering Methods. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 347-358. ISBN 978-3-540-00029-7. E-ISBN 978-3-540-36103-9. (doi:10.1007/3-540-36103-0_36) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:13646)
The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. | |
Official URL: http://dx.doi.org/10.1007/3-540-36103-0_36 |
Abstract
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.
Item Type: | Book section |
---|---|
DOI/Identification number: | 10.1007/3-540-36103-0_36 |
Additional information: | To appear |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Mark Wheadon |
Date Deposited: | 24 Nov 2008 17:59 UTC |
Last Modified: | 16 Nov 2021 09:51 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/13646 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):