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!
Ewen Denney
Last
modified: Fri May 15 11:24:40 BST 1998