We present a new approach to adding state and state-changing commands to a term language. As a formal semantics it can be seen as a generalization of predicate transformer semantics, but beyond that it brings additional opportunities for specifying and verifying programs. It is based on a construct called a phrase , which is a term of the form C ▹ t , where C stands for a command and t stands for a term of any type. If R is boolean, C ▹ R is closely related to the weakest precondition wp ( C , R ). The new theory draws together functional and imperative programming in a simple way. In particular, imperative procedures and functions are seen to be governed by the same laws as classical functions. We get new techniques for reasoning about programs, including the ability to dispense with logical variables and their attendant complexities. The theory covers both programming and specification languages, and supports unbounded demonic and angelic nondeterminacy in both commands and terms.

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 the programmer. 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 algorithmic, 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 we prove its consistency by constructing a model.

Abstract. 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.