Research on Refinement

This is a description of my research on refinement, and how I see it fitting in to the `big picture'.

To help keep things simple, I use the simply-typed lambda calculus as an idealised functional programming language. Suppose we start with a program logic, such as an equational theory for describing the input and output of functions. Some natural questions are

Some semantic questions are In my thesis, I address these questions by showing how to get a specification language and refinement calculus from the logic in a canonical way, and similarly for the semantics, giving a class of concrete (set-theoretic) models for which an applied refinement theory is indeed complete. Each model is induced in a straightforward way from a model of the programming language and program logic.

A key feature of my approach is that I construct the refinement calculus in a modular fashion, as the combination of two orthogonal extensions to the underlying programming language (in this case, just the simply-typed lambda calculus). These subcalculi are interesting in their own right as they provide separate analyses of structured specifications and what might be called `pure' refinement or (non-logical) decomposition of stubs. Formally, we introduce the concepts of refinement term and refinement type. Refinement types are a formalisation of structured specifications, and refinement terms are a formalisation of abstract programs, that is, programs with stubs for code yet to be written. `Full' refinement, then, can be factored into logical reasoning and decomposition.

The full refinement calculus is a combination of these two systems, and will be published soon.

Some Refinement Issues

Here are some of what I see as important and interesting issues relating to refinement. Some of these have been studied extensively and others have, as far as I know, not been studied at all. I think each of the above is within reach. A more fantastical aim is to develop a common logical and semantic framework for the formalisation of the entire software life-cycle, including program development, optimisation, maintenance, analysis (program comprehension) and reengineering (reverse engineering). This is not likely soon, but I do believe there's a Theory of Everything out there!

Ewen Denney

Last modified: Fri May 15 11:24:40 BST 1998