ming process itself was to be structured, not only the resulting programs. His
work encompassed step-wise refinement, and it ultimately led to the next topic
to be discussed, correctness concerns and the formal development of programs.
Until the 1970s, work on programming languages and programs was aimed
mainly at how to execute programs (or have a computer execute them), not on
how to understand programs. In 1967, Bob Floyd wrote a paper, Assigning
meanings to programs , which gave the first inklings of how one could actually
prove, mathematically speaking, that a program was correct. Tony Hoare picked
up on Floyd's work and wrote a paper (1969), An axiomatic basis for computer
programming , which provided the first definition of a programming language
that was in terms of how a program could be proved correct, rather in terms of
how it could be executed. This work was the foundation for a great deal of work
on mathematical theories of program correctness in the 1970s and 1980s. The
basic ideas found their way into programming texts as early as 1973, when
Conway and Gries provided in their text, An Introduction to Programming using
PL/I , a full account of understanding loops in terms of loop invariants.
However, at this point, the major idea was to take an existing program and
try to prove it correct, and this was extremely difficult. Far better would be to
develop a program and its proof hand-in-hand, with the proof ideas leading the
way, but the field did not know how to do this. In the mid 1970s, Edsger W.
Dijkstra published a paper and a book, A Discipline of Programming , which
indeed showed us how a program and its proof could be developed hand-in-hand.
The field of formal development of programs had emerged, and it was quite
active throughout the 1980s and 1990s. The basics of this field appear in stream-
lined form in Appendix IV, complementing our presentation of loops and loop
invariants in Chap. 7.
Throughout the 1960s and 1970s, the main feature for structuring programs
was the subroutine , or method (procedure or function), as it is now called in
object-oriented programming. Like a cooking recipe, a subroutine is simply a set
of instructions that can be invoked or called to perform some service. Until it is
invoked, or called, it does not do anything. Books on cooking are organized in
the same way that programs were organized; simply as a collection of subrou-
tines, or recipes. There were attempts to add more structure, but the basic organ-
ization was still the recipe book.
The object-oriented (OO) approach provided a new structuring mechanism,
the class (and subclass), with its principles of inheritance, instantiation, overrid-
ing, and polymorphism. The OO approach gave us a new way to think about con-
structing programs, and it actually provided a wholly new and useful mechanism
for reusing program parts.
Actually, the first OO languages, Simula I and Simula 67, were developed