A Practical Approach to Software Engineering Using Z and the Refinement Calculus

Abstract

We present a methodology for the formal specification and development of software systems using Z and the refinement calculus. The methodology combines the data structuring capabilities and the codified discrete mathematics of Z with the data encapsulation properties and development style of the refinement calculus, and it aims to provide a formal path from design to implementation without unnecessary transformations of notation or the definition of a new calculus. It is illustrated here by the development of two systems, a simply diary and (part of)a text editor, and is contrasted with the use of Z on its own. We discuss related and future work and conclude with some general comments on applied formal methods.

BibTeX

@inproceedings{Wood:FSE93,
  author    = {Kenneth R. Wood},
  title     = {A Practical Approach to Software Engineering Using Z and the Refinement Calculus},
  booktitle = {FSE},
  pages     = {79--88},
  publisher = {{ACM}},
  year      = {1993},
}

A Practical Approach to Software Engineering Using Z and the Refinement Calculus

Abstract

Related papers