Advertisement

Adding specification constructors to the refinement calculus

  • Nigel Ward
Papers
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Weak Precondition Predicate Transformer Schema Inclusion Schema Conjunction Specification Conjunction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    E. W. Dijkstra. A Discipline of Programming Prentice-Hall, 1976.Google Scholar
  3. 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. 4.
    I. J. Hayes, editor. Specification Case Studies. Series in Computer Science. Prentice-Hall, 1987.Google Scholar
  5. 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. 6.
    C. Morgan. Programming from Specifications. Series in Computer Science. Prentice-Hall, 1990.Google Scholar
  7. 7.
    C. Morgan and K. Robinson. Specification statements and refinement. IBM Journal of Research and Development, 31(5), 1987.Google Scholar
  8. 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. 9.
    J. M Spivey. The Z Notation: A Reference Manual. Series in Computer Science. Prentice-Hall, 1989.Google Scholar
  10. 10.
    M. Utting. An Object-Oriented Refinement Calculus. Phd thesis, Department of Computer Science, University of New South Wales, Sydney, 1992.Google Scholar
  11. 11.
    J. von Wright. A Lattice Theoretic Basis for Program Refinement. Phd thesis, Department of Computer Science, Åbo Akademi, 1991.Google Scholar
  12. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Nigel Ward
    • 1
  1. 1.Computer Science DepartmentUniversity of QueenslandQueenslandAustralia

Personalised recommendations