John Pinto

Document Excerpts:

It is well-known that there is only one way to establish the correctness of a computer program, namely by rigorous mathematical proof. Acceptance of this fact leaves room for two possible approaches to programming. In the first approach, a program is constructed first and its correctness is proved afterwards. This approach has two drawbacks. First, for an arbitrary program it may be very difficult, if not impossible, to prove its correctness. Second, this approach sheds no light on the methodological question how programs are to be designed.

In the second approach, advocated and developed by E.W. Dijkstra and others, the program and its proof of correctness are constructed simultaneously. Here, the obligation to construct a proof of correctness is used as a guiding principle for the design of the program. When applied rigorously, this approach can never give rise to incorrect programs; the worst thing that can happen is that no program is constructed at all because the problem is too difficult.

This document was started as a research to what extent functional programs can be designed in a calculational way. This should be possible because functional-program notations carry less operational connotations than their sequential counterparts do, functional-program notations more resemble "ordinary" mathematical formalisms than sequential-program notations do. This raised a question of whether the two ways of programming are really different: they might very well turn out to have more in common than one would expect at first sight.

The results of this research are laid down in this document. This study is about programming, as a design activity; it is not about programming languages, formal semantics included, nor about implementations. This implies that this document discusses semantics and implementations only as far as needed for its purpose, namely the formulation of a set of rules for designing programs.