Formal software development using Z and the refinement calculus

Wee, Dennis Ju-Xieng (1993) Formal software development using Z and the refinement calculus. Masters thesis, Memorial University of Newfoundland.

[English] 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. Download (17MB) [English] 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. (Original Version)

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.

Actions (login required)

View Item