Formal software development using Z and the refinement calculus

Abstract

This thesis is a study of a formal software development process that uses a formal specification language called Z [42] and the formal development method called the refinement calculus [31]. The software development process is divided into five stages: formal specification in Z, data refinement, translation into the refinement calculus, operation refinement, and translation into the target programming language [25]. In this thesis, many of the important results for understanding and using this process are collected together and numerous examples are given to illustrate their use. Through a case study of the Paragraph Problem [5, 31], we show how formality may be appropriately employed to manage the algorithmic complexity in a development, and indicate directions on how predefined programming language and library routines may be introduced into a formal development. The thesis concludes with some suggestions for further research.