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.
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.
For correct code, the information order relates (1)
what is intended and what is computed, (2) successive states of a
computation, and (3) the left and right sides of program component
definitions. For bugs, the information order is violated.
The technical results are a reasonably straightforward extension to
previous denotational semantics work, but the scheme aligns much better with
practical programming and software tools.
The theory 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