For about fifteen years, computer scientists have known how to prove that programs meet mathematical specifications.  However, the methodology has satisfied only theoreticians; "practical" programmers have tended to reject it for a variety of reasons.  Among these are the difficulty of rigorously defining the function of a program, and the fact that the proofs of correctness tend to be much longer and much more complex than the programs themselves.

We have tackled this problem from two sides.  First, we deal with proving compilers correct, a special case of programs for which there exists a rather simple specification of purpose.  Second, although we would prefer to have programs which are guaranteed to be correct, we will accept a program where we can easily determine if the output of any given run is correct.  People will generally be satisfied with a program that usually runs properly, but will always produce a message if it has not.  That way, one can have a great deal of confidence in its output.

Working with a compiler for Dijkstra's language, as defined in A Discipline of Programming, and using predicate transformers for our semantic definitions, we have presented a methodology for showing that individual compilations are correct.  This involves verifying formally the basic code templates and many library subroutines, and presenting a set of rules that allows one to perform a pattern match between the generated code and the standard templates.  This match, which is fairly easy to perform and could in fact be done by a separate program, is our guarantee that the output of the compiler is correct.

The set of rules we present includes a few restrictions on the compiler, most notably that the object code for a given statement must be uncoupled from the code for any other statement.  In general, non-optimizing compilers are not affected by any of our restrictions; our DPL compiler, which was developed independently, was not changed in any way to meet our requirements.