Verification tools in the development of provably correct compilers

  • M. R. K. Krishna Rao
  • P. K. Pandya
  • R. K. Shyamasundar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 670)


The paper presents a practical verification tool that helps in the development of provably correct compilers. The tool is based on the approach of proving termination of PROLOG-like programs using term-rewriting techniques and a technique of testing whether a given PROLOG program can be soundly executed on PROLOG interpreters without the Occur-check test. The tool has been built on top of the theorem prover, RRL (Rewrite Rule Laboratory). The tool is effective for compilers developed using Hoare's refinement algebra approach. The utility of the tool is illustrated through a case study on correctness of a prototype compiler of the ProCoS level 0 language PL0.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K.R. Apt and D. Pedreschi (1991), Reasoning about Termination of Logic Programs, Technical report, University of Pisa, September 1991.Google Scholar
  2. 2.
    K.R. Apt and A. Pellegrini (1992), Why the Occur-check is Not a Problem, in Proc. of 4th Intl. Symp. on Programming Language Implementation and Logic Programming (PLILP'92), Springer-Verlag LNCS Vol 531.Google Scholar
  3. 3.
    J. Beer (1988), The Occur-check Problem Revisited, Journal of Logic Programming, 5, pp. 243–261.CrossRefGoogle Scholar
  4. 4.
    M. Bezem (1989), Characterizing Termination of Logic Programs, Report CS-R8912, CWI, Amsterdam. Also in Proc. of North American Conf. on Logic Programming NACLP'89.Google Scholar
  5. 5.
    J. Bowen, J. He and P. Pandya (1990), An Approach to Verifiable Compiling Specification and Prototyping, in Proc. of 2nd Symp. on Programming Language Implementation and Logic Programming, PLILP'90 springer-Verlag LNCS Vol. 456.Google Scholar
  6. 6.
    P. Deransart and J. Maluszinski (1985), Relating Logic Programs and Attribute Grammers, Journal of Logic Programming 2, pp. 119–155.CrossRefGoogle Scholar
  7. 7.
    P. Deransart, G. Ferrand and M. Téguia (1991), NSTO Programs (Not Subjected To Occur-check), in Proc. Intl. Logic Programming Symp, ILPS'91, pp. 533–547.Google Scholar
  8. 8.
    N. Dershowitz (1987), Termination of Rewriting, J. of Symbolic Computation, 3, pp. 69–116.Google Scholar
  9. 9.
    N. Dershowitz and J.-P. Jouannaud (1990), Rewrite Systems, in J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, North-Holland, pp. 243–320.Google Scholar
  10. 10.
    D. De Schreye and K. Verschaetse (1992), Termination Analysis of Definite Logic Programs with respect to Call Patterns, K.U. Leuven, submitted for publication.Google Scholar
  11. 11.
    Jifeng He, P. Pandya and J. Bowen (1990), Compiling Specification for ProCoS Programming Language Level 0, ProCoS Workshop, Malente, April 1990. Also appears as Project Document, OU HJF 4/2.Google Scholar
  12. 12.
    C.A.R. Hoare (1990), Refinement Algebra Proves Correctness of Compiling Specifications, Proc. 3rd Refinement Workshop (edited by C.C. Morgan and J.C.P. Woodcock), Springer-Verlag, Workshops in Computing series, pp. 33–48.Google Scholar
  13. 13.
    C.A.R. Hoare, J. He, J. Bowen and P. Pandya (1990), An Algebraic Approach to Verifiable Compiling Specification and Prototyping of ProCoS level 0 Programming Language, Proc. of ESPRIT'90, Brussels (ed. Commission of European Communities), Kluwer Acadenuc Publishers, 1990.Google Scholar
  14. 14.
    N.D. Jones (1990), Partial Evaluation, Self-Application and Types, Proc. 17th ICALP, Springer-Verlag LNCS 443, pp. 639–59.Google Scholar
  15. 15.
    D. Kapur and H. Zhang (1989), An Overview of Rewrite Rule Laboratory (RRL), Proc. of Rewrite Techniques and Applications conference, RTA'89, Springer-Verlag LNCS vol. 355, pp 559–563.Google Scholar
  16. 16.
    M.R.K. Krishna Rao (1992), Occur-check in Well-moded Logic Programs, Proc. 7th Intl. Meeting of Young Computer Scientists, IMYCS'92, Smolenice Castle, Bratislava.Google Scholar
  17. 17.
    M.R.K. Krishna Rao, D. Kapur and R.K. Shyamasundar (1991), A Transformational Methodology for Proving termination of Logic Programs, Proc. Computer Science Logic, CSL'91, Springer-Verlag LNCS Vol. 626. pp. 213–216.Google Scholar
  18. 18.
    P. Lescanne (1983), Computer Experiments with the REVE Term Rewriting Systems Generator, in proc. 10th ACM POPL (1983), pp. 99–108.Google Scholar
  19. 19.
    J. W. Lloyd (1987), Foundations of Logic Programming, Springer-Verlag.Google Scholar
  20. 20.
    D. A. Plaisted (1984), The Occur-check Problem in Prolog, in Proc. Intl. Symp. on Logic Programming, pp. 272–280.Google Scholar
  21. 21.
    L. Pluemer (1990), Termination Proofs for Logic Programs, Ph. D. Thesis, University of Dortmund, Also appears as Springer-Verlag LNCS vol. 446.Google Scholar
  22. 22.
    L. Pluemer (1991), Automatic Termination Proofs for Prolog Programs Operating on Nonground Terms, in proc. Intl. Logic Programming Symposium, ILPS'91, pp. 503–17.Google Scholar
  23. 23.
    H. Sondergaard (1986), An Application of Abstract Interpretation of Logic Programs: Occur-check Reduction, in Proc. ESOP'86, LNCS vol. 213, pp. 327–336.Google Scholar
  24. 24.
    R.K. Shyamasundar, M.R.K. Krishna Rao and D. Kapur (1990), Rewriting Concepts in the Study of Termination of Logic Programs, Proc. ALPUK'92 conf. (edited by K. Broda), Springer-Verlag, Workshops in Computing series, pp. 3–20.Google Scholar
  25. 25.
    J.D. Ullman and A. van Gelder (1988), Efficient Tests for Top-Down Termination of Logical Rules, JACM, 35(2), pp. 345–373.CrossRefGoogle Scholar
  26. 26.
    T. Vasak and J. Potter (1986), Characterization of Terminating Logic Programs, IEEE Symposium on Logic Programming, pp. 140–147.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • M. R. K. Krishna Rao
    • 1
  • P. K. Pandya
    • 1
  • R. K. Shyamasundar
    • 1
  1. 1.Computer Science GroupTata Institute of Fundamental ResearchColaba BOMBAYINDIA

Personalised recommendations