Skip to main content
SpringerLink
Log in

Proofs in Structured Specifications

  • Chapter
Informatik und Mathematik

Abstract

Proof rules are developed for a small language that allows to write specifications in a structured and modular way. The language consists of four constructs: one for constructing a flat specification (from a signature and a set of axioms) and three operators for exporting a subsignature, for renaming and for combining specifications. Two different techniques for proving the validity of a formula in such specifications are considered. Moreover, a complete proof system for the refinement relation between specifications is established.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F.L. Bauer, H. Wössner: Algorithmic language and program development. Springer, Berlin, 1982.

    MATH  Google Scholar 

  2. F.L. Bauer, R. Berghammer, M. Broy, W. Dosch, F. Geiselbrechtinger, R. Gnatz, E. Hangel, W. Hesse, B. Krieg-Bruckner, A. Laut, T. Matzner, B. Miller, E Nickl, H. Partsch, P. Pepper, K. Samelson, M. Wirsing, H. Wössner: The Munich Project CIP, Vol. 1: The Wide Spectrum language CIP-L. Lecture Notes in Computer Science 183, Berlin, Springer, 1985.

    Google Scholar 

  3. J.A. Bergstra, J. Heering, P. Klint: Module algebra. J. ACM 37, 1990, 335–372.

    Article  MathSciNet  MATH  Google Scholar 

  4. M. Broy, P. Pepper, M. Wirsing: On relations between programs. In: B.Robinet (ed.): Proc. of the 4th International Symposium on Programming, Paris, Lecture Notes in Computer Science 83. Berlin, Springer, 1980, 59–78.

    Google Scholar 

  5. M. Broy, A. Tarlecki: Algebraic specification of the abstract data type “CONTINUUM”. EATCS Bulletin 26, June 1985, 32–35.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  8. J. Farres-Casals: Proving correctness of constructor implementations. University of Edinburgh, Dept. of Computer Science, LFCS-Report Series, ECS-LFCS-89–72, 1989.

    Google Scholar 

  9. K. Futatsugi, J.A. Goguen, J.-P. Jouannaud, J. Meseguer: Principles of OBJ2. Symposium on Principles of Programming Languages 1985, 52–66.

    Google Scholar 

  10. A. Geser, H. Huβmann: Experiences with the RAP-system–a specification interpreter combining term rewriting and resolution. In: B. Robinet, R, Wilhelm (eds.): ESOP 86. Lecture Notes in Computer Science 213, Berlin, Springer, 1986, 339–350.

    Google Scholar 

  11. J.V. Guttag, J.J. Horning, J.M. Wing: Larch in FiveFasy Pieces. Digital, Systems Research Center, Palo Alto, California, 1985.

    Google Scholar 

  12. H.B.M. Jonkers: An introduction to COLD-K. In: J.A. Bergstra, M. Wirsing (eds.): Algebraic Methods: Theory, Tools and Applications. Lecture Notes in Computer Science 394, Berlin, Springer, 1989, 139–205.

    Google Scholar 

  13. J. Leszczylowski, M. Wirsing: A system for reasoning within and about algebraic specifications. In: M. Dezani-Ciancaglini, U. Montanan (eds.): 5th International Symposium on Programming, Lecture Notes on Computer Science 137, Berlin, Springer, 1982, 257–282.

    Google Scholar 

  14. P. Padawitz: Computing in Horn Clause Theories: EATCS Monographs on Theoretical Computer Science 16, Berlin, Springer, 1988.

    MATH  Google Scholar 

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

    Google Scholar 

  16. D.T. Sannella, A. Tarlecki: Towards a formal development of programs for algebraic specifications: Implementations revisited. Acta Informatica 25, 1988, 233–281.

    Article  MathSciNet  MATH  Google Scholar 

  17. D. Sannella, M. Wirsing: A kernel language for algebraic specification and implementation. In: M. Karpinski (ed.): Colloquium on Foundations of Computation Theory. Lecture Notes in Computer Science 158. Berlin, Springer, 1983, 413–427.

    Google Scholar 

  18. M. Wirsing: Algebraic specifications of the abstract data type “continuum” without hidden operations. EATCS Bulletin 29, 1986, 46–55.

    MATH  Google Scholar 

Download references

Authors
  1. Martin Wirsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Technische Universität München, Postfach 20 24 20, W-8000, München 2, Deutschland

    Manfred Broy

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Wirsing, M. (1991). Proofs in Structured Specifications. In: Broy, M. (eds) Informatik und Mathematik. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-76677-0_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-76677-0_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-76678-7

  • Online ISBN: 978-3-642-76677-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation