We propose a new mechanism called "term transformer semantics" for giving meaning to specification and programming languages. Whereas predicate transformer semantics associates with each command a semantic function which maps boolean terms to boolean terms, our proposed semantic function maps terms of any type to terms of that same type. The old and new semantic functions coincide more or less when the arguments are boolean, and so nothing of predicate transformer semantics is lost. However, much is gained. First, we gain the glue which joins together imperative and functional programming in one uniform theory. Second, we get an elegant notation that offers new calculational possibilities for deriving programs. Its advantages for program reasoning include the availability of referential transparency, and the possibility to avoid much of the awkward use of logical variables. Third, we gain a more general invariance theorem for loops that makes reasoning about many programs easier. Fourth, we gain an elegant semantics for function procedures in the presence of nondeterministic statements. Finally,  term transformer semantics seems to offer a cleaner technical basis on which to build programming calculi such as the refinement calculus. The deployment of term transformers presupposes a theory of nondeterministic terms; we have previously developed such a theory, but term transformer semantics is independent of any particular such theory. We construct a term transformer semantics for a small but rich specimen language, and use it to illustrate fundamental properties of term transformers. We show how to build a consistency proof for a language axiomatised using term transformer semantics. Finally, we show that classical command refinement can be re-constructed more elegantly in the new semantics.

E3, EC, EB, and E4 are members of a family of many-valued logics for reasoning equationally about programs and specifications. E3 is a three-valued logic designed to handle partiality; it is more or less an equational version of typed LPF (“logic of partial functions”). EC is also three-valued, but designed to accommodate nondeterminacy rather than partiality. E4 is a four-valued logic that accommodates both partiality and nondeterminacy. EB is also four-valued, and supports nondeterminacy and miracles (i.e. empty choices); it is designed to support bunch theory. All of them are derived from the logic E of Dijkstra and Feijen. Their theory has been described elsewhere (see ''Partiality and Nondeterminacy in Program Proofs''; ''E3: A Logic for Reasoning Equationally in the Presence of Partiality'',  and ''A Theory of Bunches''). Here we prove the important theorems of the logics, and describe and justify the proof techniques that allow them to be used effectively in proof engineering. The paper is a reference manual written partly as a definitive record of the family of logics, and partly in response to the requests we have received to prove this or that theorem. Download pdf.. We also provide a quick look-up collection of the useful theorems in each logic:  Theorems of E3, Theorems of EC, Theorems of EB, and Theorems of E4.

A bunch is a simple data structure, similar in many respects to a set. As with sets, we can ask whether an element is in the data structure or not, but not how often it occurs. However, bunches differ from sets in that the data is not packaged up or encapsulated, and in particular in that a bunch consisting of one element is the same as that element.  Bunches are attractive for handling nondeterminacy and underspecification, by which is meant that for any particular input to the program or specification, the associated output is not fully determined. The acceptable outputs for any given input can be described by a bunch. This approach nicely generalises traditional single-output programs and specifications, because there is no semantic or syntactic distinction between a single value and the bunch consisting of just that value. We present a formal theory of bunches. It includes an axiomatisations of boolean and function types whose behaviour is well-known to be complicated by the presence of nondeterminacy. The axiomatisation of the booleans preserves most of the laws of classical predicate calculus. The axiomatisation of functions accommodates higher-order functions in all their generality, while avoiding the dangers of inconsistency when functions and nondeterminacy intermix. Our theory is presented as a Hilbert-style system of axioms and inference rules for a small specification language. We prove consistency.

In calculi of program specification, nondeterministic choice (some prefer ``underspecified choice'') has been found useful in writing specifications that admit a range of outcomes without constraining the implementor to just one of them. Furthermore, first-class functions have been found useful, especially for modular structuring of programs. By ``first-class'' we mean in particular that functions can be arguments to other functions and that choice is valid on function types. Together, choice and functions are good tools for writing specifications. Making a formal system accommodating both functions and choice is a difficult task. ``Obvious'' simple axioms may lead to unexpected inconsistencies. In the literature several such pitfalls are reported. In our own investigations, we have uncovered two anomalies that appear to be unknown in the literature. We examined the relevant works known to us to see whether these anomalies occur there. We have found that three of the published theories have fallen into one or the other of the traps and so are inconsistent. The remaining works avoid the traps by not facing the problems or by imposing severe restrictions on the language.

Mathematics supplies us with various operators for creating functions from relations, sets, known functions, and so on. Function inversion is a simple example. These operations are useful in specifying programs. However, many of them have strong constraints on their arguments to ensure that the result is indeed a function. For example, only functions that are bijective may be inverted. This is a serious impediment to their use in specifications, because at best it limits the specifier's expressive power, and at worst it imposes strong proof obligations on him or her. We propose to loosen the definition of functions so that the constraints on operations such as inversion can be greatly relaxed. The specificational functions that emerge generalize traditional functions in that their application to some arguments may yield no good outcome, while for other arguments their application may yield any of several outcomes unpredictably. While these functions are not in general computational, they can serve as specifications of traditional functions as embodied in programming languages. The idea of specificational functions is not new, but accommodating them in all their generality without falling foul of a myriad of anomalies has proved elusive. We investigate the technical problems that have hindered their use, and propose solutions. In particular, we develop a formal axiomatization for reasoning about specificational functions and show that it sees off the anomalies.

Partiality abounds in specifications and programs. We present a three-valued typed logic for reasoning equationally about programming in the presence of partial functions. The logic is in essence a combination of the equational logic E and typed LPF. Of course, there are already many logics in which some classical theorems acquire the status of neither-true-nor-false. What is distinctive here is that we preserve the equational reasoning style of E, as well as most of its theorems. The principal losses among the theorems are the law of the excluded middle, the anti-symmetry of implication, a small complication in the trading law for existential quantification, and the requirement to show definedness when using instantiation. The main loss among proof methods is proof by mutual implication; we present some new proof strategies that make up for this loss. Some proofs are no longer than in E, but the heuristics commonly used in the proof methodology of E remain valid. We present a Hilbert-style axiomatisation of the logic in which modus ponens and generalisation are the only inference rules. The axiomatisation is easily modified to yield a classical axiomatisation of E itself. We suggest that the logic may be readily extended to a many-valued logic, and that will have its uses.

Specifications and programs make much use of nondeterministic and/or partial expressions, i.e. expressions which may yield several or no outcomes for some values of their free variables. Traditional 2-valued logics do not comfortably accommodate reasoning about undefined expressions, and do not cater at all for nondeterministic expressions. We seek to rectify this with a 4-valued typed logic E4 which classifies formulae as either ``true'', ``false'', ``neither true nor false'', or ``possibly true, possibly false''. The logic is derived in part from the 2-valued logic E and the 3-valued LPF, and preserves most of the theorems of E. Indeed, the main result is that nondeterminacy can be added to a logic covering partiality at little cost.  Download pdf (this version corrects a small error in the published version)

Nondeterminacy is important in the formal specification and formal derivation of programs, but nondeterminacy within expressions is theoretically problematical. The refinement calculus side-steps the problem by admitting nondeterminacy only at the level of statements, leading to a style of programming that favours statements and procedures over expressions and functions. But expressions are easier to manipulate than statements, and the poverty of the expression notation has made the formal derivation of imperative programs tedious. Here we introduce nondeterministic expressions into the refinement calculus by constructing a weakest precondition semantics for imperative specifications and programs that holds good even when expressions may be nondeterministic.  Download pdf.

We present an outline of a refinement calculus for strict functional programming based on four-valued logic and equational reasoning. The language imitates the features known from the imperative refinement calculus in a language of expressions. Download pdf.

The need to apply formal specification and development of programs to large problems has highlighted a need for methods to support the modular development of specifications and their implementations. Here we present a methodology, in the framework of a type theory, that supports both these activities. We show how modular specifications may be incrementally constructed by combining individual specification units or modules with the use of appropriately defined specification building operators. We show how such modular specifications may be systematically refined to calculate an implementation. Our approach is to use a rich type theory which allows us to specify modules purely by their type. The basic theoretical notion underlying our approach is then that a specification is a type, and that an implementation of such a specification is any element in the type.

Specifications have a dual existence: on the one hand they constitute a contract between the customer and the vendor, and on the other hand they are the instructions from the vendor to his programmers. From the former viewpoint, we would like to have methods for incrementally constructing specifications, and from the second viewpoint we would like to have mechanisms for systematically "calculating" an implementation of a specification. Here we seek to develop a methodology that can give formal support to both these activities within a model-oriented framework. Indeed, these two activities, which we may call designing and refining, have much in common, and to some extent we may also "calculate" parts of a specification. The basic theoretical notion underlying our approach is that programs and specifications are more or less the same thing: a programming language is the implementable subset of a specification language. The basic practical tool we outline is a notion of modules that supports the incremental construction of specifications.  Download pdf.

"Expression refinement" is a style of specifying and programing in which expressions rather than commands are the focus of refinement. This leads to programs making much use of recursive functions and less use of loops. We illustrate the style by calculating the pattern-matching algorithm originally due to Knuth, Morris, and Pratt (KMP).  As a prelude, we calculate an interesting program that turns out to be useful in solving the KMP problem: find the maximal string that is both a suffix and a prefix of a given string.  Download pdf.

We describe by a sequence of examples a method, which we call expression refinement, for deriving programs from specifications. The method consists of making specifications using a rich notation for expressions; the expressions are then subjected to value-preserving transformations in which the rich notations are replaced by more primitive ones that are part of the implementation language. This leads to a style of programming that makes much use of recursive functions rather than loops and invariant relations. The technique is part of a larger effort to develop a fully formal and practical calculus of programming. Initial experience suggests that expression refinement is potentially a more attractive approach for formal programming than one relying principally on traditional approaches based on refinement of statements. Download pdf.

We take the view that programming consists in transforming a specification into a program according to mathematical laws that ensure that correctness is preserved. In practice, the transformation is a composition of many small transformations. To facilitate this approach, we make no formal distinction between specifications and programs: programs are merely a subset of specifications that happen to be efficiently implementable. We give specifications, and hence programs, a formal semantics by which we can define a refinement relation on them. Roughly, one specification/program refines another if its possible behaviours are a subset of the original's. The refinement relation must enjoy certain properties such as transitivity and monotonic replacement (which allows us to work on sub-parts of  a specification more or less in isolation). We describe formally a small specification/programming language in which we can elaborate on these ideas. We develop a host of useful mathematically justified transformations, and illustrate their use of a small problem. Our aim is to show that a formal calculus of programming is viable.

This paper was superseded by Laws of data refinement, Acta Informatica (26), pp. 287-308, 1989.

It is usually assumed that implementations of nondeterministic programs may resolve the nondeterminacy arbitrarily. In some circumstances, however, we may wish to assume that the implementation is in some sense fair, by which we mean that in its long-term behaviour it does not show undue bias in forever favouring some nondeterministic choices over others. Under the assumption of fairness many otherwise failing programs become terminating. We construct various predicate transformer semantics of such fairly-terminating programs. The approach is based on formulating the familiar temporal operators always, eventually, and infinitely often  as predicate transformers. We use these operators to construct a framework that accommodates many kinds of fairness, including varieties of so-called weak and strong fairness in both their all-levels and top-level forms. The semantics does not make any assumptions about the syntactic shape of programs, and allows the familiar nondeterminacy and fair nondeterminacy to be arbitrarily combined in the one program. Invariance theorems for reasoning about fairly terminating programs are proved. The semantics admits probabilistic implementations provided that unbounded fairness is excluded. Download pdf .

For C a set well-founded with respect to the partial ordering  <, and for Q.x a predicate possibly with free variable x, the theorem of well-founded induction allows us to conclude that  for all x in C, Q.x holds if it does so under the assumption that it holds for all y<x in C. Well-founded induction is very general. For example the so-called "principle of strong induction" is well-founded induction on the set of natural numbers with their usual < ordering, while so-called "transfinite induction" is well-founded induction when the ordering  <  is total. In theories of programming, proofs of properties of loops rely on well-founded induction, but the proofs may be awkward because the theorems to be proved are not typically in a form that lends themselves naturally to well-founded induction. We re-formulate well-founded induction so that we can conveniently use it to prove that Q.x holds for all x such that f(x) is in C, where  f  is any function (whose range may or may not be a subset of  C). We use  the result to make a short formula-driven proof of the fundamental invariance theorem for loops.  Download pdf.

A specification language typically contains sophisticated data types that are expensive or even impossible to implement. Their replacement with simpler or more efficiently implementable types during the programming process is called data refinement. We give a new formal definition of data refinement and use it to derive some basic laws. The derived laws are constructive in that used in conjunction with the known laws of procedural refinement they allow us to calculate a new specification from a given one in which variables are to be replaced by other variables of a different type. The underlying formal semantics is that of predicate transformers, but  the application of the laws requires no knowledge of semantics. Rather, the laws are intended as part of a larger calculus that supports the formal derivation of programs from specifications using primarily predicate calculus. The laws developed make use of the familiar technique of an abstraction invariant to relate the values of the original variables with those of the new variables. The main novelties of the work are new freedoms given in choosing abstraction invariants, and an emphasis on calculating the new specification from the old one rather than on a posteriori verification. Download pdf.