It Began with Babbage (59 page)

This approach to defining semantics came to be called
operational semantics
, because meanings of syntactic units were defined by showing the sequence of operations that would be performed on the standardized abstract machine to execute or realize that
syntactic element. The idea was a kind of formalization of the informal semantics described in English, but with respect to a formal and abstract computer.

The most developed meta-language for describing the operational semantics of a programming language was the Vienna Definition Language invented by a group at the IBM Laboratory in Vienna, inspired by McCarthy's work.
³⁶
A formal definition of the semantics of the IBM programming language PL/I was completed in 1969.
³⁷

Operational semantics for proving automatically the correctness of
microprograms
(see
Chapter 13
) would be developed during the mid 1970s.
³⁸
But, in the realm of structured programming and its concern with
humans
proving correctness of a program as it is developed, operational semantics did not excite much enthusiasm.
³⁹
The seminal work on a semantics appropriate for program verification in the structured programming context was an axiomatic method by Robert Floyd (1936–2001), who at the time was with the Carnegie Institute of Technology (later, Carnegie-Mellon University) in 1967 and, influenced by Floyd, by Anthony Hoare (1934–) in 1969, who at the time was at Queen's University, Belfast.
⁴⁰
This approach came to known as “Floyd-Hoare logic” or (more commonly)
Hoare logic
(rather as the Darwin–Wallace theory of evolution by natural selection in biology was reduced to, simply, “Darwinian evolution”).

Although Floyd used a flowchart notation, Hoare defined the axiomatic semantics of an Algol-like language. As in mathematics and logic, Hoare defined a set of axioms describing the properties of the basic syntactic entities in his language, such as the meaning of arithmetic operators and the meaning of the basic statements in the language.

To give an example of axiomatic semantics, we consider the most fundamental execution statement in Algol: the “simple” assignment statement having the general form

x
:=
E

where
x
is the identifier for a simple variable and
E
is an expression (such as an arithmetic expression). An English-language operational semantics for the assignments would be as follows: The expression
E
is evaluated; the resulting value is stored in the variable
x
. The axiomatic semantics of the assignment is as follows: If the assertion
P
(
x
), where
P
is a truth-valued function—“predicate”—with
x
as an argument, is to be true
after
the assignment is executed, then
P
(
E
) must be true immediately
before
the assignment's execution. This leads to the “axiom of assignment” expressed by the formula

{
P
₀
}
x
:=
E
{
P
}

Here,
x
is a variable,
E
is an expression, and
P
₀
is obtained from
P
by substituting
E
for all occurrences of
x
in
P
.

So if the assignment

x
:=
x +
1

leads to the assertion
P
:
x
≥ 1 after the assignment, then the assertion
P
₀
:
x
+ 1 ≥ 1
must
hold before the assignment. Notationally, this situation is represented by the H
oare formula
:

{
x
+ 1 ≥ 1}
x
: =
x
+ 1 {
x
≥ 1}

The meanings of the basic statement types in a programming language (the assignment,
if then
,
for
, and so forth, in the case of Algol 60) were given by Hoare formulas of the general form

{
P
}
S
{
Q
}. Here
P
,
Q
are true assertions and
S
is some legal program statement. The Hoare formula is to be read as follows: If the assertion
P
is true before the execution of
S
, then the assertion
Q
is true after
S
's execution.
P
and
Q
were named, respectively,
precondition
and
postcondition
.

In the manner of the axiomatic approach in mathematics and logic, Hoare logic, then, consists of axioms that define the meaning of the primitive concepts in the programming language, along with rules of inferences that define the semantics of “composite statements.” For example, the rule of sequential composition says that if for a statement
S
₁
the Hoare formula {
P
₁
}
S
₁
{
P
₂
} is true, and if for another statement
S
₂
the Hoare formula {
P
₂
}
S
₂
{
P
₃
} is true, then we may
infer
that for the sequential composition (or sequential statement)
S
₁
;S
₂
, the formula {
P
₁
}
S
₁
;S
₂
{
P
₃
} will be true.

The beauty of Hoare logic lay in that the assertions and inferences could be made on the program
text
without actually having actually to simulate the execution of the statements in the program. And we see how elegantly Dijkstra's structured programming principle can be married with Hoare logic.

As a very trivial example, consider the following sequence of assignment statements:

x
:=
x
+ 1;

y
:=
x
+
z

Suppose the variable
x
has some value symbolized as α and the variable
z
has the symbolic value β immediately before the execution of this sequence. We want to prove that after the sequence, the assertion
y
= α + β + 1 is true. We can prove this as follows:

By axiom of assignment, the Hoare formula

{
x
= α,
z
= β}
x
:=
x
+ 1 {
x
= α + 1,
z
= β}

is true. By the same axiom, the Hoare formula

{
x
= α + 1,
z
= β}
y
:=
x
+
z
{
y
= α + β + 1, x = α + 1,
z
= β}

is also true. By applying the rule of sequential composition, the Hoare formula

{
x
= α,
z
= β}
x
: =
x
+ 1;
y
: =
x
+
z
{
y
= α + β + 1,
x
= α + 1,
z
= β}

is true, in which case our objective, to show that the postcondition of the sequential statement,
y
= α + β + 1, has been proved formally.

As remarked earlier, structured programming became a fertile area of research during the 1970s. Important texts and papers would follow,
⁴¹
but the foundations were laid by Dijkstra, Floyd, and Hoare before the end of the 1960s.

  
1
. E. W. Dijkstra. (1965a). Programming considered as a human activity. In
Proceedings of the 1965 IFIP Congress
(pp. 213–217). Amsterdam: North-Holland. Reprinted in E. N. Yourdon. (Ed.). (1979).
Classics in software engineering
(pp. 3–9). New York: Yourdon Press (see especially p. 5). All citations refer to the reprint.

  
2
. Yourdon, op cit., p. 1.

  
3
. K. R. Apt. (2002). Edsger Wybe Dijkstra (1930–2002): A portrait of a genius (obituary).
Formal Aspects of Computing, 14
, 92–98.

  
4
. Quoted by Dijkstra, op cit., p. 3.

  
5
. Ibid., p. 4.

  
6
. G. H. Hardy. (1940).
A mathematician's apology
(p. 4). Cambridge, UK: Cambridge University Press.

  
7
. Dijkstra, 1965a, op cit., p. 5.

  
8
. Ibid., op cit., p. 6.

  
9
. E. W. Dijkstra. 1968a. Goto statements considered harmful.
Communications of the ACM, 11
, 147–148 (letter to the editor).

10
. Dijkstra, 1965a, op cit.

11
. E. W. Dijkstra. (1968b). The structure of the “THE” multiprogramming system.
Communications of the ACM, 11
, 341–346. Reprinted in E. Yourdon. (Ed.). (1982).
Writings of the revolution: Selected readings on software engineering
(pp. 89–98). New York: Yourdon Press (see especially p. 91). All citations refer to the reprint.

12
. Dijkstra, 1965a, op cit., p. 5.

13
. Ibid.

14
. E. W. Dijkstra. (1969). Structured programming. In J. N. Buxton, P. Naur, & B. Randell (Eds.), (1976).
Software engineering: Concepts and techniques
. New York: Litton. Reprinted in Yourdon (pp. 43–48), 1979, op cit. All citations refer to the reprint.

15
. Dijkstra, 1965a, op cit., p. 6.

16
. Ibid.

17
. Ibid.

18
. Dijkstra, 1968b, op cit.

19
. Dijkstra, 1968b, op cit., p. 91.

20
. Ibid.

21
. Ibid., 1968b, op cit., p. 92.

22
. Ibid.

23
. Ibid., pp. 95–98.

24
. Ibid., p. 92. The assumption is, though, that there will be an underlying processor available to execute a process. Thus, sequential processes are liminal rather than purely abstract artifacts.

25
. E.. W. Dijkstra. (1965b).
Cooperating sequential processes
. Technical report, Mathematics Department, Technische Universiteit Eindhoven, Eindhoven.

26
. Dijkstra, 1968b, op cit., p. 92.

27
. Ibid.

28
. Ibid., p. 97.

29
. Ibid., p. 93.

30
. E.. W. Dijkstra. (1971). Hierarchical ordering of sequential processes.
Acta Informatica, 1
, 115–138.

31
. Dijkstra, 1969, op cit., p. 44.

32
. In particular, K. R. Popper. (1965).
Conjectures and refutations
. New York: Harper & Row; K. R. Popper. (1968).
The logic of scientific discovery
. New York: Harper & Row.

33
. A. M. Turing. (1949). Checking a large routine. In Anon
Report on the conference on high-speed automatic calculating machines
(pp. 67–68). Cambridge, UK: University Mathematical Laboratory.

34
. F. L. Morris & C. B. Jones. (1984). An early program proof by Alan Turing.
Annals of the History of Computing, 6
, 139–147.

35
. J. McCarthy. (1963). Towards a mathematical science of computation. In
Proceedings of the IFIP Congress 63
(pp. 21–28). Amsterdam: North-Holland; P. J. Landin. (1964). The mechanical evaluation of expressions.
Computer Journal, 6
, 308–320.

36
. P. Wegner. (1972). The Vienna Definition Language.
ACM Computing Surveys, 4
, 5–63.

37
. O. Lucas & K. Walk. (1969). On the formal description of PL/I. In
Annual Review in Automatic Programming
(pp. 105–182). Oxford: Pergamon Press.

38
. A. Birman. (1974). On proving correctness of microprograms.
IBM Journal of Research & Development, 9
, 250–266.

39
. See, for example, J. de Bakker. (1980).
Mathematical theory of program correctness
(p. 4). London: Prentice-Hall International.

40
. R. W. Floyd. (1967). Assigning meaning to programs. In
Mathematical aspects of computer science
(Vol. XIX, pp. 19–32). Providence, RI: American Mathematical Society; C. A. Hoare. (1969). An axiomatic basis for computer programming.
Communications of the ACM, 12
, 576–580, 583.

41
. See, for example, O.-J. Dahl, E. W. Dijkstra, & C. A. R. Hoare. (1972).
Structured programming
. New York: Academic Press; D. G. Gries. (Ed.). (1978).
Programming methodology
. New York: Springer-Verlag; Yourdon, 1979, op cit.; Yourdon, 1982, op cit.

HISTORY NEVER ENDS
, despite what American political scientist Francis Fukuyama (1952–) claimed.
¹
Neither, consequently, does the writing of history. But, the writing of
a
history, like any other story, must have an ending.

The choice of where to stop a historical narrative is a matter of the narrator's judgment and, to some extent, arbitrary. English historian Edward Hallett Carr (1992–1982) famously pointed out that the historian is necessarily selective in what he or she chooses to include in the narrative.
²
That selectivity applies as much to where the narrative ends.

The story I have told here suffers from this subjectivity—both in where it begins and where it ends. This history begins in 1819, when Charles Babbage started to think about a fully automatic computing engine, and it ends in 1969—150 years later. The beginning and the ending were matters of my choice (as was everything in between). Other writers may differ in their choice of historical span as well as the contents of the history itself; but there is, I believe, a sense in where this story began and where it ended.