Adding specification constructors to the refinement calculus
- 110 Downloads
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.
KeywordsWeak Precondition Predicate Transformer Schema Inclusion Schema Conjunction Specification Conjunction
Unable to display preview. Download preview PDF.
- 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