Calculation, Transformation and Proof


Introduction

Functional programs are very close to semantic equations, and lend themselves readily to formal manipulation. New programs can be derived from old, or from specifications, or from a mixture of the two. There are various possible methods of derivation; the extension of existing methods and the invention of new ones to cope with more demanding problems is a primary topic of research. Calculating programs by hand can be tedious and error-prone, so another important topic of research is the design and implementation of semi-automatic calculators: the challenge is to combine rigour with convenience, and to enable productive co-operation between the human programmer and the mechanical assistant.

The STARSHIP system

We have combined these lines of research in STARSHIP, a prototype system that has played host to several experiments. This interactive transformation system supports fold-unfold and simple inductive proofs in a lazy polymorphic language. It can cope with a wide range of examples, including programs involving I/O. Programmed definitions and laws introduced about them automatically persist; dependencies between them are maintained, as are all outstanding proof obligations associated with each. If any assumption turns out to be false, there is automatic roll-back of exactly those derivation steps that depended on it. A form of modularity is supported, with secure transformation across module boundaries. In addition to an inbuilt command structure, a purely functional meta-language can be used to express and execute co-operative transformation strategies for machine and programmer. There is also provision for the storage, manipulation and replay of transformational histories.

Papers


York Functional Programming Group
(University of York Department of Computer Science)