Skip to main content
main-content

Über dieses Buch

This booklet presents a reasonably self-contained theory of predicate trans­ former semantics. Predicate transformers were introduced by one of us (EWD) as a means for defining programming language semantics in a way that would directly support the systematic development of programs from their formal specifications. They met their original goal, but as time went on and program derivation became a more and more formal activity, their informal introduction and the fact that many of their properties had never been proved became more and more unsatisfactory. And so did the original exclusion of unbounded nondeterminacy. In 1982 we started to remedy these shortcomings. This little monograph is a result of that work. A possible -and even likely- criticism is that anyone sufficiently versed in lattice theory can easily derive all of our results himself. That criticism would be correct but somewhat beside the point. The first remark is that the average book on lattice theory is several times fatter (and probably less self­ contained) than this booklet. The second remark is that the predicate transformer semantics provided only one of the reasons for going through the pains of publication.

Inhaltsverzeichnis

Frontmatter

Chapter 1. On structures

Abstract
The proofs in this book are much more calculational than we were used to only a few years ago. As we shall explain later, the theorems are (or could be) formulated as boolean expressions, for which, in principle, true and false are the possible values; the proofs consist in calculations evaluating these boolean expressions to true. We shall return to this later, focussing, for the time being, our attention on some of the notational consequences of this approach.
Edsger W. Dijkstra, Carel S. Schotten

Chapter 2. On substitution and replacement

Abstract
With respect to substitution and replacement, two extreme attitudes seem to prevail. Either the manipulations are deemed so simple that the author performs them without any explanation or statement of the rules, or the author tries to give a precise statement of the most general rules and ends up with 200 pages of small print, in which all simplicity has been lost. Neither is entirely satisfactory for the purposes of this little monograph.
Edsger W. Dijkstra, Carel S. Scholten

Chapter 3. On functions and equality

Abstract
We have to say a word or two about functions because, depending on the ways permitted for their definition, it may be questionable whether they are well-defined at all. Fortunately, our functions will be simple: they will be total functions with values and arguments of well-defined types.
Edsger W. Dijkstra, Carel S. Schotten

Chapter 4. On our proof format

Abstract
This chapter describes how we present our calculational proofs and, to a certain extent, why we have chosen to adopt this format.
Edsger W. Dijkstra, Carel S. Scholten

Chapter 5. The calculus of boolean structures

Abstract
In this chapter we develop the calculus of boolean structures in a rather algebraic fashion. We do so for a variety of reasons. Firstly, we have to introduce the reader to the repertoire of general formulae that will be used throughout the remainder of this booklet. Secondly, by proving all formulae that have not been postulated, we give the reader the opportunity of gently familiarizing himself with our style of conducting such calculational proofs. Thirdly, we wish to present this material in a way that does justice to how we are going to use it. Since value-preserving transformations are at the heart of our calculus, so are the notions of equality and function application; hence our desire to develop this material with the equality relation in the central rôle. (It is here that our treatment radically departs from almost all introductions to formal logic: it is not uncommon to see the equality —in the form of “if and only if”— being introduced much later as a shorthand, almost as an afterthought.)
Edsger W. Dijkstra, Carel S. Schölten

Chapter 6. Some properties of predicate transformers

Abstract
In this chapter we define and explore a number of properties that predicate transformers may or may not enjoy. It is a preparation for the later chapters in which we analyse in terms of these properties the predicate transformers that will be used to define programming language semantics. The purpose of that later analysis is to justify the procedures followed in proving properties of programs.
Edsger W. Dijkstra, Carel S. Scholten

Chapter 7. Semantics of straight-line programs

Abstract
This is a monograph about a theory of programming language semantics. Programming language definitions traditionally consist of two parts, called its “syntax” and its “semantics”, respectively.
The syntax of a programming language defines which character sequences are programs in that programming language. Moreover, the syntax defines how programs written in that programming language are to be parsed. (Fortunately, syntaxes can, in turn, be defined in several distinct steps. A meaningful separation of concerns isolates, for instance, the consequences of the fact that, ultimately, each program is expressed as a linear string of characters from a finite alphabet. One step does not distinguish between programs and their parse trees and defines which parse trees belong to the language. Another step is exclusively concerned with how the parse trees belonging to the language are coded as linear strings of characters; this step settles details such as how scopes are delineated, whether there will be infix operators, etc. This monograph being about semantics, we shall not pursue the different aspects of syntax definition.)
Edsger W. Dijkstra, Carel S. Schölten

Chapter 8. Equations in predicates and their extreme solutions

Abstract
In the previous chapter we have encountered a number of statements S for which the predicate transformers wlp.S and wp.S were given in closed form. In the next chapter we shall encounter the statement DO, for which the predicates wlp.DO.X and wp.DO.X will be defined as solutions of equations of the form
(0) Y: [b.X.Y].
Here, b is a predicate-valued function of two predicates, so [b.X. Y] is a boolean scalar that for given X and Y is either true or false. In (0) we have followed our convention —here by the prefix “Y:”— of explicitly indicating the identity of the unknown(s), and thereby notationally distinguishing between the equation and the boolean expression that forms its body.
Edsger W. Dijkstra, Carel S. Schölten

Chapter 9. Semantics of repetitions

Abstract
The reason for the inclusion of the previous chapter is that we shall use extreme solutions of equations in predicates to define the semantics of our next compound statement, known as the “repetition”. We shall first study it in its simple form, in which it is composed of a guard B and a statement S . It is denoted by surrounding the guarded statement B → S by the special bracket pair do…od . For the sake of brevity we shall call the resulting compound statement in this chapter “D0” , i.e.,
DO = do B→S od
We shall define the semantics of DO in the usual way by defining (in terms of B and S) the predicate transformers wlp.DO and wp.DO . But we shall define them differently. Were we to follow the same pattern as in the case of the straight-line programs, we would define (i) in some way the predicate transformer wlp.DO , (ii) in some way the predicate we would denote by wp.DO.true , and (iii) in terms of the previous two the predicate transformer wp.DO by
(0) [wp.DO.X = wp.DO.true Λ wlp.DO.X] for all X
Because it is more convenient, in the case of the repetition we shall follow a slightly different route: we shall define wlp.DO and wp.DO independently and then prove (0) as a consequence of those definitions. Furthermore we shall show that wlp.DO meets requirement R0 (universal conjunctivity) if wlp.S does and that wp.DO meets requirement R1 (excluded miracle) if wp.S does.
Edsger W. Dijkstra, Carel S. Schölten

Chapter 10. Operational considerations

Abstract
In the two earlier chapters on semantics, we have defined the semantics of the compound statements S0; S1, IF, and DO by defining their predicate transformers in terms of the predicate transformers of their constituent statement(s). This raises the following question. What is or could be the relation between the execution of a compound statement and the executions of its constituent statements? Or, a bit more specifically, if we know how to implement the constituent statements, how could we then implement the semicolon, the alternative construct, and the repetition? These are the questions to which this chapter is devoted. We shall deal with the three compound statements in the order in which they have been introduced. (As is only to be expected, this is also the order of increasing complexity.)
Edsger W. Dijkstra, Carel S. Schölten

Chapter 11. Converse predicate transformers

Abstract
In Chap. 7, we took the decision to define programming language semantics in terms of weakest preconditions. In our last chapter we shall return to this decision, because we can also think of such things as “strongest postconditions”. This chapter is devoted to the mathematical groundwork needed for that discussion.
Edsger W. Dijkstra, Carel S. Schölten

Chapter 12. The strongest postcondition

Abstract
From the (rather operational) introduction of Chap. 7, we recall (wlp.S)⋆.X: holds in precisely those initial states for which there exists a computation under control of S that belongs to the class “finally x”.
Edsger W. Dijkstra, Carel S. Schölten

Backmatter

Weitere Informationen