**Theo Norvell**

*How do you say what a computer program should do? How can you document
what a program does? How can you know that a program does what it should?
How do you write a program so that it does what it should?* These are
the questions that form the basis for this course. Respectively we can
call them the specification question, the documentation question, the
verification question, and the programming question.

We will take an *engineering* approach to these questions. By this I
mean that we will use mathematical tools to approach the questions with a
certain amount of rigour. We will explore the idea that, just as the
function of an electrical component can be specified by a formula such as
I=(100 +- 5)V, the function of program components can be specified by
formulas. This provides an answer to the specification question and the
documentation question. We will look at how to analyze a program in order to
extract a formula that describes its function. This provides an answer to
the verification question. We will explore the idea that we can perform
calculations with these formulas that ultimately lead us to programs. This
provides an answer to the programming question. You have already learned to
write programs, in this course you will learn to calculate them.

One way to look at the calculation of programs is to compare it to integral
calculus. In fact the mathematics that we use in this course is often called
a `programming calculus'[+].
In integral calculus one does not
(usually) guess at an integral. Instead, one starts with a formula and
manipulates it until it is in the desired form (free of integral signs). In
programming calculus the formula we start with is the `specification' and
the form we are looking for is that of a program. Traditionally programming
has been taught as a matter of making good guesses and testing the resulting
code. The analogous process in integrating is to guess a formula and *test* the resulting formula against numerical integration. The problem is
that in software a program that is correct for the vast majority of its
inputs may still be wrong. In integral calculus the process of integrating is
not entirely automatic--some steps are obvious, but to be good at
integrating takes insight and some experience. Even more so in programming.
The aim of this course is not to make programming mechanical, but to make it
formal.

The course may start to sound like a math course. It is not. The math is fairly simple but it takes some practice to learn to use it effectively -- that is to become a skilled specifier and calculator of programs.

Two books that discuss programming calculi are

- Eric C. R. Hehner,
*A Practical Theory of Programming*, Springer-Verlag, 1993. - Carroll Morgan,
*Programming from Specifications*, Prentice Hall International, 1994.

*Is correctness that important?* Bill Gates has made billions by
selling software that is full of bugs. Correctness is not always an
overriding concern. However, software is increasingly finding its
way into systems where correctness is very important. Pace-makers, flight
control and nuclear plants are
a few examples. Even when correctness is not life-critical,
the process of straining out bugs until a
system is of sufficient robustness to be sellable is often the most expensive
stage of development.
It is worthwhile to put extra effort up-front to reduce the maintenance
costs down the road. Another way to reduce maintenance costs is to
document the intended function of software components so that they may
be understood without a detailed reading of the code. Thus the course
will address the documentation problem from a formal angle.

*How will this course change your life?* This is perhaps the most
important question of all. After taking this course, I do not expect that you
will create all your future programs by calculation, nor even that you will
write a formal specification for every program (and program component) you
ever write. Engineers do not always apply the mathematics they know in
creating engineering designs. However they should have the mathematical
techniques at their disposal when they are needed. Furthermore, the most
important aspects of software engineering -- programming in the large --
will only be lightly touched on. That said, I will
mention that learning these techniques has strongly influenced my own
approach to solving all manner of programming problems even when I am
not consciously using them.

Tue Feb 13 13:31:41 NST 1996