Name
Abstract | ||
|---|---|---|
In this paper we describe an algebraic approach to construct provably correct compilers for object-oriented languages; this is illustrated for programs written in a language similar to a sequential subset of Java. It includes recursive classes, inheritance, dynamic binding, recursion, type casts and test, assignment, and class-based visibility, but a copy semantics. In our approach, we tackle the problem of compiler correctness by reducing the task of compilation to that of program refinement. Compilation is identified with the reduction of a source program to a normal form that models the execution of object code. The normal form is generated by a series of correctness-preserving transformations that are proved sound from the basic laws of the language; therefore it is correct by construction. The main advantages of our approach are the characterisation of compilation within a uniform framework, where comparisons and translations between semantics are avoided, and the modularity and extensibility of the resulting compiler. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/s00165-009-0124-9 | Formal Asp. Comput. |
Keywords | Field | DocType |
source program,refinement,algebraic transformation,provably correct compiler,resulting compiler,program refinement,object-oriented language,copy semantics,algebraic approach,normal form,basic law,compiler correctness,weakest precondition,object oriented language,virtual machine | Object code,Programming language,Dynamic compilation,Object-oriented programming,Computer science,Compiler correctness,Compiler,Theoretical computer science,A-normal form,Compiler construction,Single Compilation Unit | Journal |
Volume | Issue | ISSN |
22 | 5 | 1433-299X |
Citations | PageRank | References |
3 | 0.39 | 26 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Adolfo Duran | 1 | 10 | 3.30 |
| Ana Cavalcanti | 2 | 140 | 7.68 |
| Augusto Sampaio | 3 | 96 | 13.42 |