A refinement calculus for nondeterministic expressions

Ward, Nigel Thomas Edgar (1994). A refinement calculus for nondeterministic expressions PhD Thesis, School of Computer Science and Electrical Engineering, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
Read with bookreader  the8873.pdf Full text application/pdf 24.39MB 259
Author Ward, Nigel Thomas Edgar
Thesis Title A refinement calculus for nondeterministic expressions
School, Centre or Institute School of Computer Science and Electrical Engineering
Institution The University of Queensland
Publication date 1994
Thesis type PhD Thesis
Open Access Status File (Publisher version)
Total pages 190
Language eng
Subjects 08 Information and Computing Sciences
Formatted abstract
This thesis presents a refinement calculus for transforming highly abstract specifications into programs written in a functional programming language.

Refinement calculi allow the derivation of a program from a formal specification by a sequence of correctness-preserving transformation steps. Most refinement calculi target imperative programming languages. Functional programming languages are often more expressive than imperative programming languages. This expressive power leads to a reduced gap between the concepts used to express a problem (as a specification) and the concepts used to express its solution (as a program). Thus, a refinement calculus which targets a functional programming language can lead to a simpler development process which produces a final product more quickly.

We build a refinement calculus for functional programs by adding specification constructs to a functional language and examining transformations over the resulting language.

This thesis complements other work in the area in two major ways. Firstly, we investigate the addition of truly-nondeterministic, rather than underdetermined, choice constructs to a functional language. These constructs allow specifications which are more abstract and which admit more implementations. Secondly, most refinement calculi for functional programs add erratic choice constructs to a functional language. We investigate the addition of both demonic and angelic nondeterminism to a functional language. Demonic and erratic choice are similar: given a number of alternatives, they choose any one. In contrast, given a number of alternatives angelic choice always makes the "correct" choice, if one exists. Angelic choice is difficult to reason about, but allows the concise specification of powerful parallel constructs.
Keyword Functional programming (Computer science)
Additional Notes The University of Queensland acknowledges that the copyright owner of a thesis is its author, not the University. The University has made best endeavours to obtain author permissions to include theses in this collection, however we have been unable to trace and contact all authors. If you are the author of a thesis included in this collection and we have been unable to contact you, please email espace@library.uq.edu.au.

Document type: Thesis
Collections: Queensland Past Online (QPO)
UQ Theses (RHD) - Open Access
Version Filter Type
Citation counts: Google Scholar Search Google Scholar
Created: Thu, 14 Jan 2010, 10:52:15 EST by Ms Christine Heslehurst on behalf of Social Sciences and Humanities Library Service