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
		  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.},
  address = {Chapel Hill, NC},
  author = {Steven M. Bellovin},
  date-modified = {2017-02-16 02:27:13 +0000},
  month = {December},
  school = {Department of Computer Science, University of North
  smb-major = {yes},
  title = {Verifiably Correct Code Generation Using Predicate
  url = {https://www.cs.columbia.edu/~smb/dissabstract.html},
  year = {1982},
  bdsk-url-1 = {https://www.cs.columbia.edu/~smb/dissabstract.html}