*Introduction:* This paper outlines a method for
constructing a program together with a proof of its correctness
with respect to a given specification. The technology used is type
theory, in fact an extended version of Calculus of Constructions
Luo's ECC as implemented in Pollack's `Lego' system; here
*program* means a primitive recursive description of a
function using simply typed lambda calculus with higher order
functions and data types such as numbers and lists.

Given a precondition and a postcondition we consider pairs consisting of

- a program
- a proof that the program satisfies the postcondition given the precondition.

We call such a pair together with the pre- and postconditions a
*deliverable*, since it is what a software house should
ideally deliver to its client instead of just a program.

Now we observe that various operations, composition, pairing,
iteration and so on, can be used to combine deliverables, and that
these operations can be implemented in ECC. Consider for example
composition. If *(f, p)* is a deliverable from *pre* to
*post* and *(f', p')* is a deliverable from *post*
to *post'* then their composition is a deliverable from
*pre* to *post'* thus

*f o f'*, the composition of the functions- a proof using
*p*and*p'*that*f o f'*satisfies*post'*given*pre*.

In fact the combining operations (excluding iteration) are exactly those of a cartesian closed category whose objects are the pre- and postconditions and whose arrows are deliverables. This is comforting since it assures us that we have a complete set of combinators. They enable us to build a complicated program together with its correctness proof. Since the resulting expression of the calculus denotes a pair we can extract the program trivially by evaluating the first element of the pair.

We have used the Lego system to define these combinators and use them to create the deliverables for several programs as examples.

However in many cases a precondition and a postcondition do not satisfactorily specify a desired program. For example when developing a sorting program the precondition might ask for an arbitrary list and the postcondition demand that the result be a sorted list. But we would get little thanks for a program which always returned the nil list, even though this is sorted. We need to specify that the output list should also be a permutation of the input one.

If we try to replace the pre- and postconditions by a single
statement specifying a relation between input and output there do
not seem to be convenient combination operators; so we discard that
approach. Thinking syntactically, we could allow the pre- and
postconditions to share a free variable. For example using a free
variable *l* for lists

*pre(x) = x = l*

*post(y) = isPermutation(y, l)*

This ties the pre- and postconditions together, but such free variables should have a definite scope.

We can think, more semantically, that *l* satisfies some
base condition (it must be a list) and the pre- and post conditions
are relations whose first argument is *l*. Thus we can talk of
pre- and post conditions *relative to l*. Now a deliverable
relative to *l* is a program which takes the precondition to
the postcondition for all *l*. We will refer to these as
*second order* specifications and deliverables in contrast to
the original *first order* ones.

How should we represent specifications and deliverables in type theory? We choose the following:

A first order specification is a predicate over a type, thus

- a type,
*s*; - a function,
*S*, from*s*to*Prop*(the type of propositions);

and a first order deliverable from specification *(s, S)*
to specification *(t, T)* is a program paired with a proof
thus

- a function,
*f : s -> t*; - a proof,
*phi : forall x : s.Sx -> T(f x)*where*forall*is the Pi quantifier on propositions.

Now we can generalise these to work relative to a first order
specification *(u, U)*, which corresponds to the free variable
*l* in our example. Call *u* the base type; now the
second order specification becomes a relation over the base type
and another type, and the second order deliverable must respect the
pre- and postrelations. We leave the details to the body of the
paper.

We might try to characterise the first order deliverables as a
cartesian closed category whose objects are specifications and
whose arrows are deliverables; this is almost correct, but we have
to modify the CCC to a *semi*-cartesian closed category, a
mild generalisation due to Hayashi. The second order deliverables
are then characterised using a fibration whose fibres are
categories of first order deliverables. In fact this structure
constitutes a model of type theory.

The paper includes some illustrative examples of program development using deliverables and brief mention of others, of which the most substantial is an algorithm for the Chinese Remainder theorem.

We also discuss the relation to earlier work on extracting
programs from proofs, particularly the work of Martin-Lof as
developed by Nordstrom, Petersson and Smith. They define a
translation from a type theory, say *S*, to an underlying type
theory *U* such that the types in *S* correspond to our
specifications and the unary terms in *S* correspond to our
deliverables. A somewhat similar approach is taken by
Paulin-Mohring in her work on program extraction using the
realisability interpretation.

The virtue of our method is that it can quite easily be coded up in an existing system, and there is no difficulty about extracting the program from the proof, since they are built together but as separate components of a pair; normalising the first component gives us the program. We have mentioned operations for combining deliverables, and this might suggest a bottom-up approach; but we can just as well start with a specification of the desired program and derive the corresponding deliverable top-down by refinement in Lego.

The weakness of our method is that we have to use a combinatory
notation which is less perspicuous than the usual lambda notation
of type theory. Since deliverables form a model of type theory,
this might possibly be rectified by extending ECC with an extra
kind whose types would be specifications and whose terms would be
deliverables, thus following the insight of Martin-Lof; but we have
not yet worked out this approach. The basic approach was proposed
in an unpublished talk by Burstall at the Baastad Workshop on type
theory in 1988. A brief account by the present authors appeared as
*Deliverables: an
approach to program development in Constructions*, and a
full treatment of work so far is in McKinna's thesis.

*LFCS report ECS-LFCS-92-242,
October 1992.*

A revised version of this report was presented at Mathematical Foundations of Computing Science '93 in Gdansk. The proceedings are published by Springer-Verlag as LNCS 711, 1993.

Previous | Index | Next