A Theory of Program Refinement

Ewen Denney

Abstract:

We give a canonical program refinement calculus based on the lambda calculus and classical first-order predicate logic, and study its proof theory and semantics. The intention is to construct a metalanguage for refinement in which basic principles of program development can be studied.

The idea is that it should be possible to induce a refinement calculus in a generic manner from a programming language and a program logic. For concreteness, we adopt the simply-typed lambda calculus augmented with primitive recursion as a paradigmatic typed functional programming language, and use classical first-order logic as a simple program logic.

A key feature is the construction of the refinement calculus in a modular fashion, as the combination of two orthogonal extensions to the underlying programming language (in this case, the simply-typed lambda calculus).

The crucial observation is that a refinement calculus is given by extending a programming language to allow indeterminate expressions (or `stubs') involving the construction `some program x such that P'. Factoring this into `some x ...' and `... such that P', we first study extensions to the lambda calculus providing separate analyses of what we might call `true' stubs, and structured specifications. The questions we are concerned with in these calculi are how do stubs interact with the programming language, and what is a suitable notion of structured specification for program development.

The full refinement calculus is then constructed in a natural way as the com- bination of these two subcalculi. The claim that the subcalculi are orthogonal extensions to the lambda calculus is justified by a result that a refinement can actually be factored into simpler judgements in the subcalculi, that is, into logical reasoning and simple decomposition.

The semantics for the calculi are given using Henkin models with additional structure. Both simply-typed lambda calculus and first-order logic are interpreted using Henkin models themselves. The two subcalculi require some extra structure and the full refinement calculus is modelled by Henkin models with a combination of these extra requirements. There are soundness and completeness results for each calculus, and by virtue of there being certain embeddings of models we can infer that the refinement calculus is a conservative extension of both of the subcalculi which, in turn, are conservative extensions of the lambda calculus.

ECS-LFCS-99-412.

This report is available in the following formats:

Previous | Index | Next