De occam para o transputer: compilação via reescrita de termos
Resumo
The aim of this work is the development of a prototype compiler from occam to the transputer, in such a way that the correctness of the compiler is ensured by construction. The method used reduces the source program, through a series of algebraic transformations, to a normal form which can be directly mapped into the instructions of the target machine. Using the term rewriting facilities provided by OBJ3, the correctness proof gives as a byproduct a compiler prototype, so that at the end of the process, a running prototype will be available. This compilation method was already available, and its application was illustrated for a very simple language; our purpose here is to extend the method to deal with realistic languages and machines, such as occam and the transputer.
Referências
INMOS Ltd, Transputer instruction set: A compiler writer's guide, Prentice Hall Internacional, UK, 1988
A.W. Roscoe and C.A.R. Hoare. The Laws of Occam Programming.Theoretical Computer Science, 60:177-299, 1988.
A. Sampaio. An Algebraic Approach to Compiler Design. Phd thesis, Oxford University Computing Laboratory, 1993.
C.A.R. Hoare, He Jifeng and A. Sampaio. Normal Form Approach to a Compiler Design. Acta Informática, 30:701-739, 1993.
J. Goguen et al. Introducing OBJ. Technical report, SRI Internacional, 1993. To appear.
E. A. Scott. Automated Proof of the Correctness of a Compilling Specification. In Proceedings of Third International Conference on Algebraic Methodology and Software Technology, Workshop in Computing Series, Springer-Verlag, 1993.
S.F. Garland and J. V. Guttag. An Overview of LP, The Larch Prover. In N. Dershowitz, editor, Proceedings of the Third Internacional Conference on Rewriting Techniques and Applications (LNCS 355), pages 137-155. Springer-Verlag, 1989.
M.Broy et al. The requiriment and Design Specification Language Spectrum: An Informal Introduction. Institut Für Informatik, Techische Universitat Müncher, TUM--I9140, 1992.
W.R. Bevier, W. A. Hunt, J. S. Moore, and W. D. Young. An Approach to Systems Verification. Journal of Automated Reasoning, 5:411-428, 1989.
J. McCarthy and J.Painter. Correctness of a Compiler for Arithmetic Expressions. In Proceedings of Sumposium on Applied Mathematics. American Mathematical Society, 1967.
W. Polak. Compiler Specification and Verification. Springer-Verlag (LNCS 124), 1991.
R. Burstall and P. Landin. Programs and their Proofs: and Algebraic Approach Machine Intelligence, 7:17-43,1969.
