Skip to main content
SpringerLink
Log in
Book cover

International Symposium of Formal Methods Europe

FME 1993: FME '93: Industrial-Strength Formal Methods pp 652–670Cite as

Adding specification constructors to the refinement calculus

  • Papers
  • Conference paper
  • First Online:

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

Abstract

This paper examines how specification construction operators may be added to the refinement calculus. These operators are useful for the incremental construction of specifications of larger systems from component specifications. The overall aim is to provide a single coherent framework, in which one may both build specifications and refine these specifications to program code.

In particular, we add generalisations of Z schema conjunction and disjunction operators to the refinement calculus. These operators have been found effective for building Z specifications of substantial systems, and our aim is to provide similar facilities within the framework of the refinement calculus. The conjunction and disjunction operators are generalised so that they may be used to combine not just specification statements (the intuitive equivalent of the Z schema), but also arbitrary programs.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. J. R. Back. On the Correctness of Refinement Steps in Program Development. PhD thesis, Department of Computer Science, University of Helsinki, 1978.

    Google Scholar 

  2. E. W. Dijkstra. A Discipline of Programming Prentice-Hall, 1976.

    Google Scholar 

  3. R. Duke, P. King, G. Rose, and G. Smith. The Object-Z specification language: Version 1. Technical report 91–1, Software Verification Research Centre, Department of Computer Science, University of Queensland, 1991.

    Google Scholar 

  4. I. J. Hayes, editor. Specification Case Studies. Series in Computer Science. Prentice-Hall, 1987.

    Google Scholar 

  5. S. King. Z and the refinement calculus. In VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 164–88. Springer-Verlag, 1990.

    Google Scholar 

  6. C. Morgan. Programming from Specifications. Series in Computer Science. Prentice-Hall, 1990.

    Google Scholar 

  7. C. Morgan and K. Robinson. Specification statements and refinement. IBM Journal of Research and Development, 31(5), 1987.

    Google Scholar 

  8. J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.

    Google Scholar 

  9. J. M Spivey. The Z Notation: A Reference Manual. Series in Computer Science. Prentice-Hall, 1989.

    Google Scholar 

  10. M. Utting. An Object-Oriented Refinement Calculus. Phd thesis, Department of Computer Science, University of New South Wales, Sydney, 1992.

    Google Scholar 

  11. J. von Wright. A Lattice Theoretic Basis for Program Refinement. Phd thesis, Department of Computer Science, Åbo Akademi, 1991.

    Google Scholar 

  12. N. Ward. Draft: Adding specification constructors to the refinement calculus. In 2nd Australian Refinement Workshop. Department of Computer Science, University of Queensland, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, University of Queensland, 4072, Queensland, Australia

    Nigel Ward

Authors
  1. Nigel Ward
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

James C. P. Woodcock Peter G. Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ward, N. (1993). Adding specification constructors to the refinement calculus. In: Woodcock, J.C.P., Larsen, P.G. (eds) FME '93: Industrial-Strength Formal Methods. FME 1993. Lecture Notes in Computer Science, vol 670. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024672

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56662-5

  • Online ISBN: 978-3-540-47623-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation