Skip to main content
main-content

Über dieses Buch

Programming is a fascinating and challenging subject. Unfortunately, it is rarely presented as such. Most often it is taught by "induction": features of some famous programming languages are given operational meaning (e.g. a loop "goes round and round"), a number of examples are shown, and by induction, we are asked to develop other programs, often radically different from the ones we've seen. Basically we are taught to guess our programs, and then to patch up our guesses. Our errors are given the cute name of "bugs". Fixing them becomes puzzle-solving, as does finding tricks that exploit or avoid poorly designed features of the programming language. The entire process is time-consuming and expensive. And even so, we are never quite sure if our programs really work in all cases. When approached in this way, programming is indeed a dull activity. There is, however, another approach to programming, an approach in which programs can be developed reliably, with attention to the real issues. It is a practical approach based on methodically developing programs from their specifications. Besides being practical, it is exciting. Many programs can be developed with relative ease. Problems which once were difficult can now be solved by beginners. Elegant solutions bring great satisfaction. This is our subject. We are interested in making programming an exciting topic!

Inhaltsverzeichnis

Frontmatter

0. What can we learn from a cake?

Abstract
We are interested in programming, which in broadest terms is problem solving. There are lots of problems and we cannot solve them all. Which problems will we consider? We should delineate our topic.
Edward Cohen

1. Preliminary notions, notations, and terminology

Abstract
Formula manipulation was quite effective in solving the cake problem. In fact, if we think about it, formula manipulation has been the key to success in many areas. Civil engineers manipulate formulae in bridge design, for example.
Edward Cohen

2. Predicates A — Boolean operators

Abstract
As already mentioned, the manipulation of predicates will be our main vehicle for program development. As such, manipulating them must become second nature. This comes from practice. Throughout this chapter there are theorems whose proofs are omitted. Although these proofs are exercises at chapter end, we highly recommend attacking them as they appear in the text. They are a lot of fun, and will be of great help in absorbing the material. Attacking theorems whose proofs are included will be of great help too.
Edward Cohen

3. Predicates B — Quantified expressions

Abstract
For symmetric and associative binary0 operators op we write the quantified version of op as
$$\left( {\underline {OP} {\text{ }}i:R:T} \right)$$
(0)
Expression (0) is called a quantified expression, or a quantification for short. Its type is the same as the type of op: if op is an arithmetic operator, then (0) is a boolean expression, and so on.
Edward Cohen

4. Specifications

Abstract
What do we do when asked to construct a “customer database”. At first glance the problem seems straightforward enough. Upon closer inspection many questions arise: what characterizes a customer?, what functions must be provided?, and so on. Given to ten different people, ten different solutions will appear, and it is entirely likely that none will provide what was desired. The problem, of course, is that “customer database” is much too imprecise.
Edward Cohen

5. The shapes of programs

Abstract
The activity of programming is the activity of solving a specification for its unknown, where this unknown is called a program. Programs are formulae of a certain shape.
Edward Cohen

6. Intermezzo on calculations

Abstract
In the next chapter we embark on our study of programming. What we will find is that most of it boils down to calculation and, as such, an effective programmer must first be an effective calculator.
Edward Cohen

7. Developing loopless programs

Abstract
The activity of programming is the activity of solving a specification for its unknown. A specification’s unknown is called a program. This chapter marks the beginning of our study of programming. Here we constrain ourselves to the development of programs that contain no loops. In subsequent chapters we study the development of loops. For now we concentrate on the assignment and the IF. We will discover that the development of assignments and IFs are mainly matters of straightforward calculation!
Edward Cohen

8. Developing loops — an introduction

Abstract
Our insight into developing loops comes from the Invariance Theorem:
$$ \begin{array}{*{20}{c}} {\left\{ P \right\}\underline {do} B \to S\underline {od} \left\{ {P \wedge \neg B} \right\}} \\ { \Leftarrow {\text{ the conjuction of}}} \end{array}$$
(0)
$$ \left\{ {P \wedge B} \right\}S\left\{ P \right\}$$
(a)
$$ \left\{ {P \wedge B \wedge t = T} \right\}S\left\{ {t < T} \right\}$$
(b)
$$P \wedge t \leq 0 \Rightarrow \neg B$$
(c)
where P is a predicate called a loop invariant, and t is an integer function called the bound function. Conjunct (a) is the requirement of Invariance, conjunct (b) is the requirement of Progress, and conjunct (c) is the requirement of Boundedness.
Edward Cohen

9. Loops A — On deleting a conjunct

Abstract
The first step in developing a loop is to choose an invariant (and a guard). In particular, given postcondition R, invariant P and guard B must be chosen to satisfy
$$P \wedge \neg B \Rightarrow R.$$
(0)
Edward Cohen

10. Loops B — On replacing constants by fresh variables

Abstract
The first step in loop development is to choose invariant P and guard B from postcondition R to satisfy
$$P \wedge \neg B \Rightarrow R$$
If R happens to be a conjunction, then this is easy. Choose for P one of the conjuncts, and choose for B the negation of the other conjunct, as we have seen.
Edward Cohen

C11. Mainly on recursion

Abstract
Many functions are defined recursively. Consider exponentiation: for integer x and natural y, we have
$$\begin{gathered} {x^y} = \,\underline {fi} \,y = \,0\, \to \,1 \hfill \\ \,\,\,\,\,\,\,\,\,\,{\text{}}\,\,\,{\text{y}} \ne {\text{0}}\, \to \,x\, * \,{x^{y - 1}} \hfill \\ \,\,\,\,\,\,\,\,\,\,\underline {fi} \hfill \\ \end{gathered}$$
In other words, exponentiation is defined recursively.
Edward Cohen

12. Back to scratch

Abstract
In previous chapters we were asked to solve specifications for their programs. The specifications were given. Practicing programmers, however, are rarely given specifications. Usually we get informal problem statements.
Edward Cohen

13. Where to go from here

Abstract
We have seen a number of methods. We have applied these methods to a number of examples. While the examples were not the subject matter, I have tried to choose generally useful ones.
Edward Cohen

Backmatter

Weitere Informationen