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
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.