On the role of interpolation in stepwise refinement.

T. Dimitrakos and T.S.E. Maibaum

Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ

ftd,tsemg@doc.ic.ac.uk

Abstract

In the 25 years of its history, basic research in the Abstract Data Type community has been challenged to provide answers to some critical questions on the fundamentals of refinement between formal specifications. Such questions include: Why do correct refinements not compose correctly in all cases ? What results are dependent on the specification formalism (equational, first order, etc) and what are universal"? Which meta-logical properties of a specification formalism facilitate the refinement process? An example of a metalogical property which amounts to a law" of a general theory of specification and refinement is given by the role of interpolation in parameter instantiation and the composability of refinements. In addition, the presence of a Uniform version of Craig-Robinson interpolation is shown in [9] to facilitate the verification and construction of refinements and to underlie the potential automation of the refinement process in an appropriate entailment system.

1 A refinement paradigm
Let us consider program development by means of stepwise refinements. One postulates some abstract data type-like specification1 (ADT), suitable for the problem at hand, which has to be implemented on the available system. The end product consists of (the text of) an abstract program manipulating the postulated ADT, together with a suite of (texts of) modules implementing successive ADTs on more concrete ones until reaching the available executable level (Target Programming Platform", TPP). See also [18, 16, 23]. The essential knowledge about the relevant properties of the abstractions involved, is provided by the axioms in the specifications. The proof that the abstract program does exhibit the required behaviour consists of syntactical manipulations that derive the verification conditions from the abstract specification. Similarly, the correctness of the implementations of the ADTs is verified by syntactical processes, as

1Refinement of abstract data types has been the original motivation. In the context of this paper, the generic term ADT may also refer to program and systems specifications.

we shall elaborate upon in the sequel.

A closer examination of what is involved when implementing an ADT S on (in terms of) another one T, indicates that the resulting artifact is a module M that represents objects of S in terms of those of T, and operations and predicates of S by means of procedures using operations and predicative statements of T. One can abstract a little from the actual procedure texts by replacing them with specifications of their input-output behaviours. These amount to possibly incomplete definitions of the operations and predicates in S in terms of those of T and can be regarded as axioms involving both the symbols of S and T. Similarly the representation part describes the abstract" sorts in terms of the concrete" ones, which can be abstracted to axioms introducing the new sorts and capturing (some of) the so-called representation invariants [15, 17].

With this abstraction in mind, we are ready to describe this situation in terms of formal specifications, ie. logical theories presented by (finite sets of) axioms [34, 33].

One expands the language of the concrete" specification T by adding symbols to correspond to the abstract ones in S, perhaps together with some auxiliary symbols, and extends T to M by adding extension axioms which are sentences in the extended language. Since one does not want to disturb the given concrete specification T, the extension e from T to M should not impose any new constraints on T. This is formulated by requiring the extension e:T!M to be conservative [26] in the sense that M adds no consequence to T in the language of the latter.

One then needs to correlate the abstract" symbols in S to the corresponding ones in T (similarly, in some sense, to procedure headings / calls being correlated with the corresponding bodies). However, the properties of S are still important, for instance in guaranteeing the correctness of the abstract program described by S. Thus, in translating from S to M one wishes to preserve the properties of S as specified by its axioms. Hence, the translation