Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Provably correct compiler development and implementation

  • Conference paper
  • First Online:

Abstract

This paper reports on provably correct compiler implementation in the ESPRIT basic research action 3104 ProCoS (Provably Correct Systems). A sharp distinction is drawn between correctness of the specification of a compiler and correctness of the actual implementation. The first covers semantical correctness of the code to be generated, whereas the second concerns correctness of the compiler program with respect to the specification. The compiler construction framework presented aims at minimizing the amount of handcoding during implementation and at reusing specification correctness arguments for proving the implementation correct. The classical technique of bootstrapping compilers is revisited with respect to implementation correctness.

This work has been partially funded by the Commission of the European Communities under ESPRIT Basic Research Action 3104 ProCoS (Provably Correct Systems).

Similar content being viewed by others

Keywords

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.

References

  1. Dines Bjørner et al.Final Deliverable of the ProCoS Project. Computer Science Department, Technical University of Denmark, Lyngby, DK, 1992 (submitted to Springer Verlag for publication)

    Google Scholar 

  2. Dines Bjørner, Cliff B. Jones.The Vienna Development Method: The Meta Language. LNCS 61. Springer Verlag, 1978

    Google Scholar 

  3. R.S. Boyer, J S. Moore.A Computational Logic Handbook. Academic Press, 1988

    Google Scholar 

  4. Martin Fränzle.Verification of Compilers for Recursive occam-like Languages. Master's Thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, FRG, 1990

    Google Scholar 

  5. C.A.R. Hoare.Communicating Sequential Processes. Prentice-Hall Int., 1985

    Google Scholar 

  6. C.A.R. Hoare.Refinement Algebra Proves Correctness of Compiling Specifications. PRG-TR-6-90. Programming Research Group, Oxford University, UK, 1990

    Google Scholar 

  7. inmos Limited.Transputer instruction set: A compiler writers guide. Prentice-Hall Int., 1988

    Google Scholar 

  8. inmos Limited.occam 2 Reference Manual. Prentice-Hall Int., 1988

    Google Scholar 

  9. Cliff B. Jones.Systematic Software Development Using VDM. Prentice-Hall Int., 1990

    Google Scholar 

  10. Yassine Lakhneche.Equivalence of Denotational and Structural Operational Semantics of PL. Master's Thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, FRG, 1991

    Google Scholar 

  11. Markus Müller-Olm.Correctness Proof of SubLISP to PL Translation. Master's Thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, FRG, 1990

    Google Scholar 

  12. W. Polak.Compiler Specification and Verification. LNCS 124. Springer Verlag, 1981

    Google Scholar 

  13. Joseph E. Stoy.Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977

    Google Scholar 

  14. W.D. Young.A mechanically verified code generator. Journal of Automated Reasoning, 5(4), December 1989

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, Preußerstr. 1-9, D-2300, Kiel, FRG

    Bettina Buth, Karl-Heinz Buth, Martin Fränzle, Burghard v. Karger, Yassine Lakhneche, Hans Langmaack & Markus Müller-Olm

Authors
  1. Bettina Buth

    You can also search for this author inPubMed Google Scholar

  2. Karl-Heinz Buth

    You can also search for this author inPubMed Google Scholar

  3. Martin Fränzle

    You can also search for this author inPubMed Google Scholar

  4. Burghard v. Karger

    You can also search for this author inPubMed Google Scholar

  5. Yassine Lakhneche

    You can also search for this author inPubMed Google Scholar

  6. Hans Langmaack

    You can also search for this author inPubMed Google Scholar

  7. Markus Müller-Olm

    You can also search for this author inPubMed Google Scholar

Editor information

Uwe Kastens Peter Pfahler

Rights and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Buth, B.et al. (1992). Provably correct compiler development and implementation. In: Kastens, U., Pfahler, P. (eds) Compiler Construction. CC 1992. Lecture Notes in Computer Science, vol 641. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55984-1_14

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp