# dissertation.bib

@phdthesis{bellovin:verifiably,
abstract = {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 \emph{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.},