While simple equational reasoning is adequate for the calculation of many algorithms from their functional specifications, it is not up to the task of dealing with others, particularly those specified as optimisation problems. One approach is to replace functions by relations, and equational reasoning by reasoning about relational inclusion. But such a wholesale approach means one has to adopt a new and sometimes subtle language to argue about the properties of relational expressions. A more modest proposal is to generalise our powers of specification by allowing certain nondeterministic, or multi-valued functions, and to reason about refinement instead. Such functions will not appear in any final code. Refinement calculi have been studied extensively over the years and our aim in this article is just to explore the issues in a simple setting and to justify the axioms of refinement using the semantics suggested by Morris and Bunkenburg.
展开▼
