Refinement and Re-use

Abstract

Transformations, by definition, are reversible. Working purely with transformations is therefore essentially about re-arranging information, and without some particular strategies (such as those given in Chapter 3) we run the risk of going round in circles and wasting much effort getting precisely nowhere. Even when our initial specification is deterministic (and hence specifies a single function rather than a collection of functions, any one of which would be acceptable in the eyes of the specifier), we may well wish to introduce intermediate non-determinism within the process of deriving a correct implementation of a specified function. This is in line with the software engineering maxim that decisions should be delayed for as long as possible. We have already met a common instance of this in the application of structural splitting to the processing of lists; instead of deciding exactly how a list should be split, we can simply say that L should be split into, say L₁ and L₂, so that

. For non-trivial lists, there are many ways that this can be done — and therefore we have nondeterminism, which must eventually be resolved. Subsequent processing of L₁ and L₂ will generally lose details of these lists, and consequently any attempt to retrieve L and then decompose it in a different way may be impossible. In this small, but very important, chapter we give the essential elements of the theory of Operational Refinement (or Functional Refinement) based on the notion of the progressive reduction of non-determinism. We start with the basic formalisation in Section 6.1