Andy Gravell's Papers

A selection of published papers. Praise or other comments gratefully received!

Publications since 2000

Recent papers can be found on the ECS e-prints system

Verification Conditions are Code

This paper presents the theoretical underpinnings of the next one, in the form of a main theorem supported by 9 lemmas and definitions. The result shows that the verification conditions of a Hoare style proof can be used, together with the pre- and post-condition, to generate code. Some small examples are given and the significance of the result discussed. A later version of this paper was published in Acta Informatica, volume 43, pages 431--477, 2006.

Logical Refinement: generating imperative programs from verified conditions

This paper presents a radically different approach to formal program development in which the proof genuinely comes first, and all the code is automatically generated from a set of purely logical formulas. A prototype code generator has been implemented in Prolog.

What is a Good Specification?

Most interesting problems can be specified in many different but equivalent ways. Which of this is to be preferred depends on your sense of style. This paper investigates the choices that arise in writing a formal specification and suggests some guidelines that may help authors. The most important point is that, if readers of a specification are to have confidence in its validity, it must contain formal definitions and informal narrative that correspond closely, so that they can be checked. I am grateful to Eerke Boiten from the University of Kent at Canterbury for pointing out an error in this paper; in section 2.3 it is wrongly claimed that a certain set theoretic equation is equivalent to the simpler equation known = dom birthday.

Abbreviating Z

This paper lists 8 possible extensions to standard Z. Each proposed extension abreviates a construct that occurs commonly in specifications. Most of the abbreviations are in fact based on notations used in other areas of computing and mathematics. In particular the Z notation would benefit from the elegant and powerful notations available to functional programmers. As well as making specifications more concise, these extensions would make Z more familiar, and thus more acceptable, to workers in other areas of computing.

Executing Formal Specifications Need Not Be Harmful

This paper discusses the various arguments that have been advanced for and against the use of executable specifications. We give examples of the problems which may arise in applying this technique, and of the benefits which may accrue. There are circumstances where execution can be of high value, but it must be used as a supplement to other methods of validating specifications such as inspection and proof.

A First Order Refinement Calculus

In this thesis a first order notation, ZF', is developed. This is a conservative extension of ZF set theory based loosely on the Z notation. ZF' can be used for specification, programming and formal program derivation. The subset of ZF' that supports programming includes functions, procedures, recursion and abstract state machines. Refinement is supported by an extensive collection of laws for both operation and data refinement. Examples of the notation, and comparisons with other existing notations and methods, are made throughout. It is concluded that a first order refinement calculus provides a good fit with a first order model-based specification notation such as Z or ZF'.

Common Errors in Z Specifications

Writing a good formal specification is not the same as writing a good program. The criteria are different. A fair amount of advice has now been written on how to write good specifications. Yet students of the Z notation continue to make elementary mistakes which suggest that they have not fully understood this advice. This short paper attacks this problem in a different way: rather than showing students good specifications which they are supposed to emulate, why not show them some bad specifications and explain what is wrong with them? It is perhaps easier to avoid the typical errors if you know what they are.

Simpler Laws for the Introduction of Loops

This paper concerns the refinement calculus of Carroll Morgan and in particular his loop introduction law which, it is claimed, is rather difficult to use. This means that derivations involving the introduction of loops tend to be long and convoluted. This paper makes three modest suggestions that help to shorten and simplify these derivations in particular situations. The suggestions are illustrated with the help of simple example derivations. Finally comparisons are made with alternative approaches.

The Case for Total Programming

This paper considers total functions, which are uniformly defined, total procedures (or batch programs), which terminate uniformly, and total processes, which consist of a UNITY-like set of total procedures, so that they never terminate. This collection is shown to be Turing-complete. It can also appropriate for interactive programming. The paper argues from a software engineering viewpoint that total programming improves the reliability of programs, and makes them easier to reason about, with only a minor sacrifice of expressiveness. In particular, considering only total programs allows definitions and laws to be simplified. Formal derivations of total procedures are given using a novel combination of the Z-style termination convention combined with partial correctness reasoning. The derivations, it is claimed, are at least as clear and simple as those produced by other methods of formal operational refinement.

Andy Gravell, September 2002.