A Mathematical Theory of Correct Computation
Lee Naish, Bernard Pope, Harald Søndergaard
In 1970, Dana Scott proposed his highly influential "mathematical
theory of computation" to define the relationship between the text of a
program and what the program computes (or denotes) - the "semantics"
of the program. Scott used a complete lattice based on the "information
ordering", with the bottom element representing undefined - a program
failing to terminate normally, thus producing no information. The top
element, however, was unused. Hence most subsequent applications of
denotational semantics have used mathematical structures that avoid
top elements. We suggest that the information ordering is relevant not
only to semanticists, but also to working programmers, as a basis for
determining if a program component or a computation is correct according
to their intentions. We also suggest that a return to the use of complete
lattices is called for if we wish to broaden formal semantics to allow it
to encompass programmer intentions. That is because often those intentions
permit more than one runtime behaviour for a given input. For example,
several declarative debugging tools allow a programmer to declare
that a runtime call is "inadmissible", loosely meaning the called
program component should never be used with such input. If the input
is garbage, the programmer does not care what garbage is output -
all results are acceptable, which can be modeled by the top element of
a complete lattice. In this paper we explore the connections between
the information ordering, correctness of computations and programs, and
debugging. We present a general theory and describe several instances
where the intention for what our logic/functional code computes plus
what it actually computes can be described by elements in a complete
lattice. This extends both the theoretical basis and practical flexibility
of declarative debugging and reasoning about partial correctness and gives
an attractive mathematical framework that encompasses our intentions,
our programs and what they compute.
Keywords:
logic programming
; functional programming
; semantics
; partial correctness
; declarative debugging
; specification
; information ordering
; complete lattice
Lee