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.

[img] [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 (16Mb)
  • [img] [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.

Item Type: Thesis (Masters)
URI: http://research.library.mun.ca/id/eprint/4280
Item ID: 4280
Additional Information: Bibliography: leaves 163-166.
Department(s): Science, Faculty of > Computer Science
Date: 1993
Date Type: Submission
Library of Congress Subject Heading: Z (Computer program language); Computer software--Development

Actions (login required)

View Item View Item

Downloads

Downloads per month over the past year

View more statistics