# 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

• What is a suitable specification language, based on the program logic, for the purposes of program development?
• How can we formalise specification testing, that is, checking whether the specification guarantees any program which satisfies it to have certain properties? This is a form of prototyping.
• What minimal extensions to the lambda calculus can give a refinement calculus?
Some semantic questions are
• From a model of the programming language and the program logic, can we get a model of the refinement calculus?
• Can we describe a class of models for which the refinement calculus is complete, that is, the calculus proves a refinement if and only if it is true in all the models?
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.

• Extending a programming language with stubs gives an internalisation of the stage of program development. The language of refinement terms is studied in the paper Simply-typed Underdeterminism.
• Extending the program logic to give a structured specification language, where the formal specifications are refinement types is carried out in the paper Refinement Types for Specification.
• An earlier and more comprehensive version is Refining Refinement Types.
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.
• Are there substantial differences between refinement calculi for different computational paradigms, such as functional and imperative languages?
• Automated code generation : Although the program development process can never be fully automated, it could be partially supported by theorem provers. A theorem prover for specification and refinement should be induced by one for the underlying logic.
• It goes without saying that an integrated environment for specification, testing and development is necessary. A tool should be able to record and manipulate entire derivations.
• Extension to richer computational scenarios : The work described here is complicated enough (for me) yet is restricted to the simplest possible situation. It should be possible to extend it in a systematic way to account for other computational features, such as concurrency, exceptions, probabilistic nondeterminism. A further problem is how to combine logics to give a `heterogeneous' refinement calculus.
• Recording and manipulating derivations : By treating a derivation as a first class object, we can facilitate program comprehension and reengineering (reverse engineering). By recording the insights that went into developing the program, the code is more easily understood.
• Refinement between specifications in different formalisms : Information systems can be specified using many different formalisms, especially at different stages of the software development life-cycle. Examples are data flow diagrams, entity relationship diagrams, and algebraic specifications. It is important to be able to relate these different forms of specification. This is especially important for ensuring that a functional specification matches the requirements specification. Semantic methods, notably category theory, should help here. I don't think a `mother of all type theories' approach will help.
• A notion of refinement for general information systems (such as databases).
• Software reuse : One of the main advantages of a refinement framework is that keeping a record of the development of a program will help when using the code to implement a different specification.
• Object-oriented analysis and design : There are three main classes of popular analysis and design methods : process, data and object-oriented. The two main kinds of refinement are program and data refinement. A corresponding notion of object refinement does not, however, appear to have been extensively studied. This would be especially interesting because iterative prototype development in OOD has similarities to refinement.
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!