Wee, Dennis Ju-Xieng (1993) Formal software development using Z and the refinement calculus. Masters thesis, Memorial University of Newfoundland.
PDF (Migrated (PDF/A Conversion) from original format: (application/pdf))
- Accepted Version
Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission.
This thesis is a study of a formal software development process that uses a formal specification language called Z  and the formal development method called the refinement calculus . 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 . 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.
|Item Type:||Thesis (Masters)|
|Additional Information:||Bibliography: leaves 163-166.|
|Department(s):||Science, Faculty of > Computer Science|
|Library of Congress Subject Heading:||Z (Computer program language); Computer software--Development|
Actions (login required)