A refinement calculus for nondeterministic expressions
Nigel Ward · The University of Queensland · 1994
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.