Skip to main content
SpringerLink
Log in

Proof systems for structured algebraic specifications: An overview

  • Invited Lectures
  • Conference paper
  • First Online:
Book cover Fundamentals of Computation Theory (FCT 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1279))

Included in the following conference series:

Abstract

In this paper an overview on proof systems for structured algebraic specifications is presented. As underlying language we choose an ASL-like kernel language which includes reachability and observability operators. Three different kinds of proof systems are studied. The first two approaches are non-compositional systems where the basic idea is to compute for any structured specification a flat unstructured set of axioms and rules which, combined with some standard proof systems for the underlying logic, may be used for deriving theorems of the specification. In the normal form approach of Bergstra, Hering and Klint, a flat set of axioms is constructed for each structured specification, whereas in the second approach not only individual axioms but also individual proof rules are taken into account. The drawback of the non-compositional proof systems is that they do not reflect the modular structure of specifications. Therefore we present also a structured proof system the derivations of which are performed in accordance with the modular structure of a specification.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. A. Bergstra, J. Heering, P. Klint: Module algebra. Journal of the Association for Computer Machinery 37 (2), 335–372,1990.

    Google Scholar 

  2. M. Bidoit, R. Hennicker: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science 165 (1), 3–55, 1996.

    Article  Google Scholar 

  3. R. M. Burstall: Proving properties of programs by structural induction. Computer Journal 12, 41–48, 1969.

    Google Scholar 

  4. R. M. Burstall, J. A. Goguen: The semantics of CLEAR, a specification language. In: Proc. Advanced Course on Abstract Software Specifications, Springer Lecture Notes in Computer Science 86, 292–332, 1980.

    Google Scholar 

  5. M. V. Cengarle: Formal specifications with higher-order parameterization. Dissertation, Institut für Informatik, Universität München, Aachen, Verlag Shaker, 1995.

    Google Scholar 

  6. N. Dershowitz, J. P. Jouannaud: Rewriting systems. In: J. van Leeuwen (ed.): Handbook of Theoretical Computer Science, Vol. B, Amsterdam, North-Holland, 1990.

    Google Scholar 

  7. H. Ehrig, B. Mahr: Fundamentals of Algebraic Specification 1, EATCS Monographs on Theoretical Computer Science 6, Springer, 1985.

    Google Scholar 

  8. J. Farrés-Casals. Verification in ASL and related specification languages. Ph.D. thesis, Report CST-92-92, University of Edinburgh, 1992.

    Google Scholar 

  9. R. Harper, D. T. Sannella, A. Tarlecki: Structure and representation in LF. Proc. 4th IEEE Symp. on Logic in Computer Science, Asilomar, 226–237, 1989.

    Google Scholar 

  10. R. Harper, D. T. Sannella, A. Tarlecki: Structured theory presentations and logic representations. Annals of Pure and Applied Logic 67, 113–160, 1994.

    Article  Google Scholar 

  11. R. Hennicker: Structured specifications with behavioural operators: semantics, proof methods and applications. Habilitation thesis, Institut für Informatik, Universität München, 1997.

    Google Scholar 

  12. R. Hennicker, M. Wirsing, M. Bidoit: Proof systems for structured specifications with observability operators. Theoretical Computer Science 173, 393–443, 1997.

    Article  Google Scholar 

  13. H. J. Keisler. Model theory for infinitary logic. North-Holland, 1971.

    Google Scholar 

  14. G. Kreisel, J. L. Krivine: Eléments de Logique Mathematique. Dunod (Paris), 1967.

    Google Scholar 

  15. T. S. E. Maibaum, P. A. S. Veloso, M. R. Sadler: A theory of abstract data types for program development: Bridging the gap? In: H. Ehrig, C. Floyd, M. Nivat, J. Thatcher (eds.): Proc. TAPSOFT '85, Joint Conference on Theory and Practice of Software Development, Springer Lecture Notes in Computer Science 186, 214–230, 1985.

    Google Scholar 

  16. G. Malcolm, J. A. Goguen: Proving correctness of refinement and implementation. Technical Monograph PRG-114, Oxford University Computing Laboratory, 1994.

    Google Scholar 

  17. E. Mendelson: Introduction to Mathematical Logic. Mathematics Series. Wadswort & Brooks/Cole, 3rd edition, 1987.

    Google Scholar 

  18. P. D. Mosses: CoFI: The common framework initiative for algebraic specification and development. In: Proc. TAPSOFT '97, Theory and Practice of Software Development, Springer Lecture Notes in Computer Science 1214, 115–137, 1997.

    Google Scholar 

  19. H. Peterreins: A natural-deduction-like calculus for structured specifications. Dissertation, Institut für Informatik, Universität München, 1996.

    Google Scholar 

  20. D. T. Sannella, R. M. Burstall: Structured theories in LCF. In: G. Ausiello, M. Protasi (eds.): 8th CAAP, L'Aquila, Springer Lecture Notes in Computer Science 159, 377–391, 1983.

    Google Scholar 

  21. D. T. Sannella, A. Tarlecki: Toward formal development of ML programs: foundations and methodology. In: J. Diaz, F. Orejas (eds.): Proc. TAPSOFT '89, Springer Lecture Notes in Computer Science 352,375–389,1989.

    Google Scholar 

  22. D. T. Sannella, M. Wirsing. A kernel language for algebraic specifications and implementation. In: M. Karpinski (ed.): Proc. FCT'83, Springer Lecture Notes in Computer Science 158, 413–427, 1983.

    Google Scholar 

  23. O. Schoett: Behavioural correctness of data representation. Science of Computer Programming 14, 43–57, 1990.

    Article  Google Scholar 

  24. M. Wirsing: Algebraic specification. In: J. van Leeuwen (ed.): Handbook of Theoretical Computer Science, Amsterdam, North-Holland, 675–788, 1990.

    Google Scholar 

  25. M. Wirsing: Structured specifications: syntax, semantics and proof calculus. In: F. L. Bauer, W. Brauer, H. Schwichtenberg (eds.): Logic and Algebra of Specification, International Summer School Marktoberdorf, 1991, Springer, 411–442, 1993.

    Google Scholar 

  26. M. Wirsing: Algebraic specification languages: an overview. In: E. Astesiano, G. Reggio, A. Tarlecki (eds.): Recent Trends in Data Type Specification. Proc. 10th Workshop on Specification of Abstract Data Types. Springer Lecture Notes in Computer Science 906, 81–115, 1995. *** DIRECT SUPPORT *** A0008123 00002

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Ludwig-Maximilians-Universität München, Oettingenstr. 67, D-80538, München, Germany

    Rolf Hennicker & Martin Wirsing

Authors
  1. Rolf Hennicker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Wirsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Bogdan S. Chlebus Ludwik Czaja

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hennicker, R., Wirsing, M. (1997). Proof systems for structured algebraic specifications: An overview. In: Chlebus, B.S., Czaja, L. (eds) Fundamentals of Computation Theory. FCT 1997. Lecture Notes in Computer Science, vol 1279. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0036169

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63386-0

  • Online ISBN: 978-3-540-69529-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation