Skip to main content
SpringerLink
Log in

Upgrading the pre- and postcondition technique

  • Papers
  • Conference paper
  • First Online:
VDM'91 Formal Software Development Methods (VDM 1991)

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

Included in the following conference series:

Abstract

This paper gives a reconstruction of the classical pre- and postcondition technique from its roots and extends it with several features. A number of problems in connection with pre- and postcondition specifications are discussed and solutions presented. Problems that are discussed include: framing, dynamic object creation, non-atomic actions and user-friendly syntax. The technique as described is part of the specification language COLD-1 and has been used in several industrial applications.

This work has been performed within the framework of ESPRIT project 2565 (ATMOSPHERE).

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. E.W. DIJKSTRA, A Discipline of Programming, Prentice Hall (1976).

    Google Scholar 

  2. L.M.G. FEIJS, H.B.M. JONKERS, C.P.J. KOYMANS, G.R. RENARDEL DE LAVALETTE, Formal Definition of the Design Language COLD-K, Technical Report, ESPRIT project 432 (1987).

    Google Scholar 

  3. J.G. GROENENDIJK, M. STOKHOF, Dynamic Predicate Logic, University of Amsterdam (1989).

    Google Scholar 

  4. D. HAREL, First-order Dynamic Logic, Lecture Notes in Computer Science 68, Springer-Verlag (1979).

    Google Scholar 

  5. C.A.R. HOARE, An axiomatic basis for computer programming, Communications of the ACM 12 (1969), 576–580.

    Google Scholar 

  6. C.B. JONES, Systematic Software Development using VDM, Second Edition, Prentice Hall (1989).

    Google Scholar 

  7. H.B.M. JONKERS, The single linguistic framework, Technical Report, ESPRIT pilot project FAST (1984).

    Google Scholar 

  8. H.B.M. JONKERS, An Introduction to COLD-K, in: M. WIRSING, J.A. BERGSTRA (Eds.), Algebraic Methods: Theory, Tools and Applications, LNCS 394, Springer-Verlag (1989), 139–205.

    Google Scholar 

  9. H.B.M. JONKERS, Description of COLD-1, Technical Report, ESPRIT project 2565 (1991).

    Google Scholar 

  10. C.P.J. KOYMANS, G.R. RENARDEL DE LAVALETTE, The Logic MPLω, in: M. WIRSING, J.A. BERGSTRA (Eds.), Algebraic Methods: Theory, Tools and Applications, LNCS 394, Springer-Verlag (1989), 247–282.

    Google Scholar 

  11. C.A. MIDDELBURG, Syntax and Semantics of VVSL, Ph.D. Thesis, University of Amsterdam (1990).

    Google Scholar 

  12. R. SARACCO, J.R.W. SMITH, R. REED, Telecommunications Systems Engineering using SDL, North-Holland (1989).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Philips Research Laboratories Eindhoven, P.O. Box 80000, 5600, JA Eindhoven, The Netherlands

    H. B. M. Jonkers

Authors
  1. H. B. M. Jonkers
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Prehn W. J. Toetenel

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jonkers, H.B.M. (1991). Upgrading the pre- and postcondition technique. In: Prehn, S., Toetenel, W.J. (eds) VDM'91 Formal Software Development Methods. VDM 1991. Lecture Notes in Computer Science, vol 551. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54834-3_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-54834-3_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54834-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation