Skip to main content
SpringerLink
Log in

Assertional Data Reification Proofs: Survey and Perspective

  • Conference paper
4th Refinement Workshop

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

In this survey we discuss three methods for program development, which incorporate data reification: VDM, Reynolds’ method, and Back’s method and develop a modest predicate transformer based framework to relate them. At first we consider partial correctness only, and discuss Reynolds’ method and a partial correctness version of VDM. Later we also consider total correctness in order to cover (part of) Back’s refinement calculus and the full notion of specification and associated refinement methods in VDM.

Supported by NWO/SIGN Project 612-316-022: “Fault Tolerance: Paradigms, Models, Logics, Construction.”

Partially supported by ESPRIT project 3096: “SPEC.”

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. M. Abadi & L. Lamport. The Existence of Refinement Mappings. Proceedings of the 3rd IEEE Conference on Logic in Computer Science (LICS), pp. 165–175, 1988.

    Google Scholar 

  2. K.R. Apt. Ten Years of Hoare’s Logic: A Survey—Part I. ACM Transactions on Programming Languages and Systems 4: 431–483, 1981.

    Article  Google Scholar 

  3. R.J.R. Back. On the Correctness of Refinement Steps in Program Development. Report A-1978–4, Dept. of Computer Science, University of Helsinki, 1978.

    Google Scholar 

  4. R.J.R. Back. Data Refinement in the Refinement Calculus. Reports on computer science & mathematics 68, Abo Akademi, 1988.

    Google Scholar 

  5. R.J.R. Back & J. von Wright. Refinement Calculus, Part I: Sequential Non deterministic Programs. In Stepwise Refinement of Distributed Systems, LNCS 430, pp. 42–66. Springer-Verlag, 1990.

    Google Scholar 

  6. R.J.R. Back. Refinement Calculus, Part II: Parallel and Reactive Programs. In Stepwise Refinement of Distributed Systems, LNCS 430, pp. 67–93. Springer-Verlag, 1990.

    Google Scholar 

  7. J.W. de Bakker, G. Rozenberg & W.-P. de Roever. Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings of the NFI/REX Workshop, LNCS 430. SpringerVerlag 1990.

    Google Scholar 

  8. N.W.P. van Diepen Si W.-P. de Roever. Program Derivation through Transformations: The Evolution of List-Copying Algorithms. Science of Computer Programming 6:213–272, 1986.

    Google Scholar 

  9. P. Gardiner & C. Morgan. A Single Complete Rule for Data Refinement, submitted to ACM Transactions on Programming Languages and Systems.

    Google Scholar 

  10. S.L. Gerhart. Correctness Preserving Program Transformations. Proceedings 2nd Symposium on Principles of Programming Languages, pp. 54–66, 1975.

    Google Scholar 

  11. D. Gries. The Science of Programming. Springer-Verlag, 1981.

    Google Scholar 

  12. He Jifeng. Process Simulation and Refinement. Formal Aspects of Computing 1:229–241, 1989.

    Google Scholar 

  13. E.C.R. Hehner. The Logic of Programming. Prentice-Hall, 1984.

    Google Scholar 

  14. E.C.R. Hehner. Predicative Programming Part I. Communications of the ACM 27: 134–143, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  15. E.C.R. Hehner. Predicative Programming Part II. Communications of the ACM 27: 144–151, 1984.

    Article  MATH  Google Scholar 

  16. C.A.R. Hoare. Proofs of Correctness of Data Representation. Acta Informatica 1: 271–281, 1972.

    Article  MATH  Google Scholar 

  17. C.A.R. Hoare, He Jifeng & J.W. Sanders. Prespecification in Data Refinement. Information Processing Letters 25: 71–76, 1987.

    Article  MathSciNet  Google Scholar 

  18. C.B. Jones. Software Development: a Rigorous Approach. Prentice-Hall, 1980.

    Google Scholar 

  19. L. Lamport. Specifying Concurrent Program Modules. ACM Transactions on Programming Languages and Systems 2: 190–220, 1983.

    Article  Google Scholar 

  20. S. Lee, W.-P. de Roever & S.L. Gerhart. The Evolution of List-Copying Algorithms and The Need for Structured Program Verification. Conf. Rec. 6th Ann. ACM Symp. on Principles of Progr. Languages, pp. 53–67, 1979.

    Google Scholar 

  21. R. Milner. An Algebraic Definition of Simulation between Programs. Proceedings of 2nd Int. Joint Conf. on Artificial Intelligence, pp. 481–489, 1971.

    Google Scholar 

  22. C. Morgan. Programming from Specifications. Prentice-Hall, 1990.

    Google Scholar 

  23. J.M. Morris. Laws of data refinement. Acta Informatica 26: 287–308, 1989.

    MathSciNet  MATH  Google Scholar 

  24. E.-R. Olderog. On the Notion of Expressiveness and the Rule of Adaptation. Theoretical Computer Science 24: 337–347, 1983.

    Article  MathSciNet  MATH  Google Scholar 

  25. J.C. Reynolds. The Craft of Programming. Prentice-Hall, 1981. 114

    Google Scholar 

  26. C.B. Jones. Systematic Software Development using VDM, 2nd edition. Prentice-Hall, 1989.

    Google Scholar 

  27. J. Zwiers. Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and Their Relationship. LNCS 321, Springer-Verlag, 1989.

    Google Scholar 

  28. J. Zwiers. Predicates, Predicate Transformers and Refinement. In Stepwise Refinement of Distributed Systems, LNCS 430, pp. 759776. Springer-Verlag, 1990.

    Google Scholar 

  29. J. Zwiers & W.-P. de Roever. Predicates are Predicate Transformers: A Unified Compositional Theory for Concurrency. To appear in the proc. of Principles of Distributed Computing ’89.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Math. and Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    J. Coenen

  2. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, D-2300, Kiel, Fed. Rep. Germany

    W.-P. de Roever

  3. University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands

    J. Zwiers

Authors
  1. J. Coenen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. W.-P. de Roever
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. Zwiers
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, University of Glasgow, G12 8QQ, Glasgow, Scotland

    Joseph M. Morris PhD

  2. Lloyd’s Register House, Lloyd’s Register of Shipping, 29 Wellesley Road, CR0 2AJ, Croydon, Surrey, UK

    Roger C. Shaw

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coenen, J., de Roever, WP., Zwiers, J. (1991). Assertional Data Reification Proofs: Survey and Perspective. In: Morris, J.M., Shaw, R.C. (eds) 4th Refinement Workshop. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3756-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3756-6_5

  • Publisher Name: Springer, London

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

  • Online ISBN: 978-1-4471-3756-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation