next up previous contents index
Next: Physical Characteristics Up: Overview Previous: Evaluation

Programming Modes

The   term_of operation enables two new modes of programming in in addition to the conventional mode of writing function terms. To program in the first new mode one writes proof outlines, p, which contain the computational information necessary for term_of(p) to be executable. The second mode is a refinement of the first in which complete proofs, cp, are supplied as arguments to term_of. In this case one knows that the program meets its specification, so this mode might be called ``verified programming''.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995