Skip to main content
Springer Nature Link
Log in

Experiences with software specification and verification using LP, the Larch proof assistant

  • Published:
Save article
View saved research
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We sketch a method for deduction-oriented software and system development. The method incorporates formal machine-supported specification and verification as activities in software and systems development. We describe experiences in applying this method. These experiences have been gained by using the LP, the Larch proof assistant, as a tool for a number of small and medium size case studies for the formal development of software and systems. LP is used for the verification of the development steps. These case studies include

  • • quicksort

  • • the majority vote problem

  • • code generation by a compiler and its correctness

  • • an interactive queue and its refinement into a network.

The developments range over levels of requirement specifications, designs and abstract implementations. The main issues are questions of a development method and how to make good use of a formal tool like LP in a goal-directed way within the development. We further discuss the value of advanced specification techniques, most of which are deliberately not supported by LP and its notation, and their significance in development, Furthermore, we discuss issues of enhancement of a support system like LP and the value and the practicability of using formal techniques such as specification and verification in the development process in practice.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+
from €37.37 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Price includes VAT (Netherlands)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

References

  1. J.W. de Bakker, W.-P. de Roever, and G. Rozenberg (Eds.),Stepwise Refinement of Distributed Systems, Lecture Notes in Computer Science 430, Springer 1990.

  2. W.R.Bevier, “Kit and the short stack,”Journal of Automated Reasoning, Vol 5, pp. 519–530, 1989.

    Google Scholar 

  3. B. Boyer and J. Moore, “MJRTY: A fast majority algorithm,” Unpublished.

  4. M.Broy, “Views of queues,”Science of Computer Programming, Vol. 11, pp. 65–88, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  5. M. Broy, “Functional specification of time sensitive communicating systems,”REX Workshop, in [1]. pp. 153–179.

  6. M. Broy,Experiences with Software Specification and Verification Using LP, The Larch Proof Assistant, Digital Systems Research Center, SRC Report 93, November 1992.

  7. M. Broy,Algebraic Methods for Program Construction, The Project CIP. SOFSEM 82, also in, P. Pepper (Ed.),Program Transformation and Programming Environments, NATO ASI Series, Series F: 8, Berlin-Heidelberg-New York-Tokyo, Springer, pp. 199–222, 1984.

    Google Scholar 

  8. L. Cardelli and P. Wegner, “On understanding types, data abstraction, and polymorphism,”ACM Computing Survey, pp. 471–523, 1985.

  9. L.Cardelli, “Basic polymorphic typechecking,”Science of Computer Programming, Vol. 8, pp. 147–172, 1987.

    Article  MATH  Google Scholar 

  10. U. Fraus and H. Hußmann, “A narrowing-based theorem prover (extended abstract),” in4th International Conference on Rewriting Techniques and Applications (RTA), Como, Italy, Lecture Notes in Computer Science, Vol. 488, Springer-Verlag 1991, pp. 435–436.

    Google Scholar 

  11. S.J. Garland and J.V. Guttag,An Overview of LP, The Larch Prover, Lecture Notes in Computer Science, Vol. 355, pp. 137–151, 1986.

  12. S.J. Garland, J. V. Guttag, and J.J. Horning,Debugging Larch Shared Language Specifications, Digital Systems Research Center, SRC Report, 60, July 1990.

  13. S.J. Garland and J.V. Guttag,A Guide to LP, The LARCH Prover, Digital Systems Research Center, SRC Report 82, December 1991.

  14. A. Geser and H. Hußmann, “Experiences with the RAP system—A specification interpreter combining term rewriting and resolution,” in B. Robinet and R. Wilhelm (Eds.),ESOP 86 Conference Proceedings, Lecture Notes in Computer Science, 213, Springer, 1986, pp. 339–350.

  15. J.V.Guttag, J.J.Horning, and J.Wing, “An overview of the larch family of specification languages,”IEEE Software, Vol. 2, No. 5, pp. 24–36, 1985.

    Google Scholar 

  16. J.V.Guttag and J.J.Horning, “Report on the larch shared language,”Science of Computer Programming, Vol. 6, No. 2, pp. 103–134, 1986.

    Article  MATH  Google Scholar 

  17. J.V.Guttag and J.J.Horning, “A larch shared language handbook,”Science of Computer Programming, Vol. 6, No. 2, pp. 135–157, 1986.

    Article  MATH  Google Scholar 

  18. J.V.Guttag and J.J.Horning (Eds.), S.J.Garland, K.D.Jones, A.Modet, and J.M.Wing, “Larch: languages and tools for formal specification,”Texts and Monographs in Computer Science, Springer-Verlag, New York, 1993.

    Google Scholar 

  19. C.A.R.Hoare, “Quicksort,”Computer Journal, Vol. 5, pp. 10–15, 1962.

    Article  MATH  MathSciNet  Google Scholar 

  20. C.A.R.Hoare and M.Foley, “Proof of a recursive program: Quicksort,”Computing Journal, Vol. 14, No. 4, pp. 391–395, 1971.

    Article  MATH  MathSciNet  Google Scholar 

  21. H. Hußmann, “A case study towards algebraic verification of code generation,” in T. Rus and C. Rattray (Eds.),2nd Conference on Algebraic Methodology and Software Technology (AMAST), Iowa City, Iowa, USA, to appear in Springer Workshops in Computer Science, May 1991.

  22. C.B. Jones,Systematic Program Development Using VDM, Prentice Hall, 1986.

  23. R. London,Correctness of Two Compilers for a LISP Subset. Stanford University, Computer Science Department, CS 240, October 1971.

  24. D.MacKenzie, “The fangs of the VIPER,”Nature, Vol. 352, pp. 467–468, 1991.

    Article  Google Scholar 

  25. M.S. Manasse and G. Nelson,Correct Compilation of Control Structures.

  26. J.Misra and D.Gries, “Finding Repeated Elements,”Science of Computer Programming, Vol. 2, pp. 143–152, 1982.

    Article  MATH  MathSciNet  Google Scholar 

  27. T. Nipkow, “Term rewriting and beyond—Theorem proving in Isabelle,”Formal Aspects of Computing, Vol. 1, pp. 320–338.

  28. A. C. Reeves,Towards a Sketch Based Model of Self-Interpreters, University of Stirling, Ph.D. Thesis, Submitted September 1991.

  29. T. Rus,Algebraic Construction of a Compiler, The University of Iowa, Department of Computer Science, Technical Report 90-01, February 1990.

  30. B. Schieder, Private Communication.

  31. The MunichSpectrum Group, M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hußmann, D. Nazareth, F. Regensburger, and K. Stølen,The Requirement and Design Specification Language Spectrum,An Informal Introduction, Institut für Informatik, Technische Universität München, TUM-19140, October 1991.

  32. M. Wirsing, “Algebraic specification,”Handbook of Theoretical Computer Science, 1990.

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, D-80290, München, Germany

    Manfred Broy

Authors
  1. Manfred Broy
    View author publications

    Search author on:PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Broy, M. Experiences with software specification and verification using LP, the Larch proof assistant. Form Method Syst Des 8, 221–272 (1996). https://doi.org/10.1007/BF00709138

Download citation

  • Received:

  • Revised:

  • Issue date:

  • DOI: https://doi.org/10.1007/BF00709138

Keywords