Abstract
This paper generalizes an algebraic method for the design of a correct compiler to tackle specification and verification of an optimized compiler. The main optimization issues of concern here include the use of existing contents of registers where possible and the identification of common expressions. A register table is introduced in the compiling specification predicates to map each register to an expression whose value is held by it. We define different kinds of predicates to specify compilation of programs, expressions and Boolean tests. A set of theorems relating to these predicates, acting as a correct compiling specification, are presented and an example proof within the refinement algebra of the programming language is given. Based on these theorems, a prototype compiler in Prolog is produced.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Aho, A. V., Sethi, R. and Ullman, J. D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Series in Computer Science, 1986.
Bjørner, D.: Trusted Computing Systems: The ProCoS Experience. Proc. ICSE ’14, North-Holland, Melbourne, Australia, 11–14 May 1992.
Bowen, J. P.: From Programs to Object Code using Logic and Logic Programming. In [GiG92], pp. 173–192.
Bowen, J. P.: From Programs to Object Code and back again using Logic Programming: Compilation and Decompilation. Journal of Software Maintenance: Research and Practice, 5, 205–234 (December 1993).
Bowen, J. P. et al.: A ProCoS II Project Description: ESPRIT Basic Research Project 7071. Bulletin of the European Association for Theoretical Computer Science (EATCS), 50, 128–137 (June 1993).
Bowen, J. P. (ed.): Towards Verified Systems. Elsevier, Real-Time Safety-Critical Systems series, 1994.
Bowen, J. P. and Breuer, P. T: Occam’s Razor: The Cutting Edge of Parser Technology. Proc. TOULOUSE’92: Fifth International Conference on Software Engineering and its Applications, Toulouse, France, 7–11 December 1992.
Bowen, J. P. and Breuer, P. T.: Decompilation. In van Zuylen, H. (ed.), The REDO Compendium: Reverse Engineering for Software Maintenance, chapter 10, John Wiley & Sons, pp. 131–138, 1993.
Bowen, J. P., Fränzle, M., Olderog, E.-R. and Ravn, A.P.: Developing Correct Systems. Proc. 5th Euromicro Workshop on Real-Time Systems, IEEE Computer Society Press, pp. 176–187, 1993.
Bowen, J. P., He Jifeng and Pandya, P. K.: An Approach to Verifiable Compiling Specification and Prototyping. In Deransart, P. and Małuszyński, J. (eds.), Programming Language Implementation and Logic Programming, Springer-Verlag, LNCS 456, pp. 45–59, 1990.
Bowen, J. P. and Stavridou, V.: Safety-Critical Systems, Formal Methods and Standards. IEE/BCS Software Engineering Journal, 8(4), 189–209 (July 1993).
Breuer, P. T. and Bowen, J. P.: Decompilation is the Efficient Enumeration of Types. In Billaud, M. et al. (eds.), Journées de Travail WSA’92 Analyse Statique, BIGRE 81-82, IRISA-Campus de Beaulieu, F-35042 Rennes cedex, France, pp. 255–273, 1992.
Bundy, A., Smaill, A. and Wiggins G.: The Synthesis of Logic Programs from Inductive Proofs. In Lloyd, J. W (ed.) Computational Logic. pringer-Verlag, Basic research series, pp. 135–149, 1990.
Bunimova, E. O.: A Method of Language Mappings Describing. Doctoral dissertation, Moscow University, Russia, 1982. (In Russian.)
Buth, B., Buth, K.-H., Fränzle, M., von Karger, B., Lakhneche, Y., Langmaack, H. and Müller-Olm, M.: Provably Correct Compiler Implementation. In Karstens, U. and Pfahler, P. (eds.), Compiler Construction, Springer-Verlag, LNCS 641, pp. 141–155, 1992.
Clement, T. P. and Lau, K.-K.: Logic Program Synthesis and Transformation. Springer-Verlag, Workshops in Computing, 1992.
Clocksin, W. F., and Mellish, C. S.: Programming in Prolog. 3rd edition, Springer-Verlag, 1987.
Cohen, J.: Constraint Logic Programming Languages. Communications of the ACM, 33(7), 52–68 (1990).
Curzon, P.: Deriving Correctness Properties of Compiled Code. Formal Methods in System Design, 3, 83–115 (1993).
Giegerich, R.: Considerate Code Selection. In [GiG92], pp. 51–65.
Giegerich, R. and Graham, S. L. (eds.): Code Generation — Concepts, Tools, Techniques. Springer-Verlag, Workshops in Computing, 1992.
He Jifeng and Bowen, J. P.: Time Interval Semantics and Implementation of a Real-Time Programming Language. Proc. Fourth Euromicro Workshop on Real-Time Systems, IEEE Computer Society Press, pp. 110–115, 1992.
He Jifeng, Page, I. and Bowen, J. P.: Towards a provably correct hardware implementation of Occam. In Milne, G. J. and Pierre, L. (eds.) Correct Hardware Design and Verification Methods, Springer-Verlag, LNCS 683, pp. 214–225, 1993.
Hoare, C. A. R.: Refinement Algebra Proves Correctness of Compiling Specifications. In Morgan, C. C. and Woodcock, J. C. P. (eds.), 3rd Refinement Workshop, Springer-Verlag, Workshops in Computing, pp. 33–48, 1991.
Hoare, C. A. R. and He Jifeng: Refinement Algebra Proves Correctness of a Compiler. In Broy, M. (ed.), Programming and Mathematical Method, Springer-Verlag, NATO ASI Series F: Computer and Systems Sciences, vol. 88, pp. 245–269, 1992.
Hoare, C. A. R., He Jifeng, Bowen, J. P. and Pandya, P. K.: An Algebraic Approach to Verifiable Compiling Specification and Prototyping of the ProCoS Level 0 Programming Language. ESPRIT ’90 Conference Proceedings, Kluwer Academic Publishers, pp. 804–818, 1990.
Hoare C. A. R., He Jifeng and Sampaio, A.: Normal Form Approach to Compiler Design. Acta Informatica, 30, 701–739 (1993).
Krishna Rao, M. R. K., Pandya, P. K. and Shyamasundar, R. K.: Verification Tools in the Development of Provably Correct Compilers. In Woodcock, J. C. P. and Larsen, P. G. (eds.), FME ’93: Industrial-Stength Formal Methods, Springer-Verlag, LNCS 670, pp. 442–461, 1993.
Levin, V.: Algebraically Provable Specification of Optimized Compilations. In Bjørner, D., Broy, M. and Pottosin, I.V. (eds.), Formal Methods in Programming and Their Applications, Springer-Verlag, LNCS 735, 1993.
Lloyd, J. W: Foundations of Logic Programming. 2nd edition, Springer-Verlag, 1987.
Russinoff, D. M.: A Verified Prolog Compiler for the Warren Abstract Machine. Journal of Logic Programming, 13, 367–412 (1992).
Stepney, S.: High Integrity Compilation: A Case Study. Prentice Hall, 1993.
Stepney, S., Whitley, D., Cooper, D. and Grant, C.: A Demonstrably Correct Compiler. Formal Aspects of Computing, 3(1), 58–101 (January–March 1991).
Author information
Authors and Affiliations
Corresponding author
Additional information
Funded by ESPRIT Basic Research ProCoS project (nos 3104 & 7071).
Funded by UK Engineering and Physical Sciences Research Council (SAFEMOS project IED3/1/1036 and grant no. GR/J15186).
Rights and permissions
About this article
Cite this article
Jifeng, H., Bowen, J. Specification, Verification and Prototyping of an Optimized Compiler. Form Asp Comp 6, 643–658 (1994). https://doi.org/10.1007/BF03259390
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF03259390