Advertisement

Compiler Correctness and Input/Output

  • Paul Curzon
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 8)

Abstract

We describe the formal machine-checked verification of a compiler from a subset of the Vista structured assembly language to the flat assembly language Visa. In particular, we describe the problems associated with input and output commands. We present an oracle based model of I/O. We show how this model can be incorporated into both the relational semantics of Vista and the interpreter semantics of Visa. We illustrate how the compiler correctness theorem proved is sufficient to deduce correctness properties of compiled code from properties of the original program.

Keywords

Semantic Relation Target Language Assembly Language High Order Logic Total Correctness 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    W. R. Bevier, Jr., W. A. Hunt, W. D. Young. Towards verified execution environments. Proc. of the 1987 IEEE Symp. on Security and Privacy, 1987.Google Scholar
  2. [2]
    A. Cohn. A proof of correctness of the Viper microprocessor: The first level. VLSI Specification, Verification and Synthesis, G. Birtwistle, P. A. Subrahmanyam Eds., Kluwer Academic Publishers, 1988, pp. 1-91.Google Scholar
  3. [3]
    A. Cohn. Correctness properties of the Viper block model: The second level. Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle, P. A. Subrahmanyam Eds., Springer-Verlag, 1989, pp. 27-72.Google Scholar
  4. [4]
    W. J. Cullyer. Implementing safety critical systems: The Viper Microprocessor. VLSI Specification, Verification and Synthesis, G. Birtwistle, P. A. Subrahmanyam Eds., Kluwer Academic Publishers, 1988, pp. 1-25.Google Scholar
  5. [5]
    P. Curzon. A verified compiler for a structured assembly language. Proc. of the 1991 Int. Workshop on the HOL Theorem Proving System and its Applications, IEEE Computer Society Press, 1992, pp. 253-262.Google Scholar
  6. [6]
    P. Curzon. A programming logic for a verified structured assembly language. Logic Programming and Automated Reasoning, A. Voronkov Ed., Lecture Notes in Artificial Intelligence Vol. 624, Springer-Verlag, 1992, pp. 403-408.Google Scholar
  7. [7]
    P. Curzon. Deriving correctness properties of compiled code. Proc. of the 1992 Int. Workshop on Higher Order Logic Theorem Proving and its Applications, L. Claesen, M. Gordon Eds., 1992.Google Scholar
  8. [8]
    J. Despeyroux. Proof of translation in natural semantics. IEEE Symp. on Logic in Computer Science, 1986, pp. 193-205.Google Scholar
  9. [9]
    M. J. C. Gordon. Mechanizing programming logics in higher order logic. Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle, P. A. Subrahmanyam Eds., Springer-Verlag, 1989, pp. 387-439.Google Scholar
  10. [10]
    M. J. C. Gordon, T. F. Melham Eds. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1992.Google Scholar
  11. [11]
    C. A. R. Hoare, N. Wirth. An axiomatic definition of the programming language PASCAL. Acta Informatica, Vol. 2, 1973, pp. 335–355.CrossRefGoogle Scholar
  12. [12]
    C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall Int., 1985.Google Scholar
  13. [13]
    J. J. Joyce. A verified compiler for a verified microprocessor. Technical Report 167, University of Cambridge, Computer Laboratory, March 1989.Google Scholar
  14. [14]
    J. J. Joyce. Generic specification of digital hardware. Technical Report 90-27, The University of British Columbia, Department of Computer Science, September 1990.Google Scholar
  15. [15]
    J. J. Joyce. Private communication. 1990.Google Scholar
  16. [16]
    J. Kershaw. Vista user’s guide. Technical Report 401-86, RSRE, 1986.Google Scholar
  17. [17]
    D. Martin, R. Toal. Case studies in compiler correctness using HOL. Proc. of the 1991 Int. Workshop on the HOL Theorem Proving System and its Applications, IEEE Computer Society Press, 1992, pp 242-252.Google Scholar
  18. [18]
    J. McCarthy, J. Painter. Correctness of a compiler for arithmetic expressions. Proc. of Symp. in Applied Mathematics, J. T. Schwartz Ed., Vol. XIX, 1966, pp. 33-41.Google Scholar
  19. [19]
    T. F. Melham. Abstraction mechanisms for hardware verification. VLSI Specification, Verification and Synthesis, G. Birtwistle and P. A. Subrahmanyam Eds., Kluwer Academic Publishers, 1988, pp. 267-292.Google Scholar
  20. [20]
    J. S. Moore. A mechanically verified language implementation. Journal of Automated Reasoning, Vol. 5, 1989, pp. 461–492.Google Scholar
  21. [21]
    G. D. Plotkin. A structural approach to operational semantics. Technical report, University of Aarhus, Denmark, Computer Science Department, 1981.Google Scholar
  22. [22]
    W. Polak. Compiler Specification and Verification. Lecture Notes in Computer Science Vol. 124, Springer-Verlag, 1981.Google Scholar
  23. [23]
    T. G. Simpson. Design and verification of IFL: a wide-spectrum intermediate functional language. Technical Report 91/440/24, The University of Calgary, Department of Computer Science, July 1991.Google Scholar
  24. [24]
    S. Stepney, D. Whitley, D. Cooper, C. Grant. A demonstrably correct compiler. Formal Aspects of Computing, Vol. 3, 1991, pp. 58–101.MATHCrossRefGoogle Scholar
  25. [25]
    W. D. Young. A mechanically verified code generator. Journal of Automated Reasoning, Vol. 5, 1989, pp. 493–519.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Wien 1993

Authors and Affiliations

  • Paul Curzon
    • 1
  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeUK

Personalised recommendations