Toward formal development of programs from algebraic speci cations: parameterisation revisited Donald Sannellay Stefan Sokolowskiz Abstract Andrzej Tarleckix Parameterisation is an important mechanism for structuring programs and speci cations into modular units. The interplay between parameterisation (of programs and of speci cations) and speci cation (of parameterised and of non-parameterised programs) is analysed, exposing important semantic and methodological di erences between speci cations of parameterised programs and parameterised speci cations. The extension of parameterisation mechanisms to the higher-order case is considered, both for parameterised programs and parameterised speci cations, and the methodological consequences of such an extension are explored. A speci cation formalism with parameterisation of an arbitrary order is presented. Its denotational-style semantics is accompanied by an inference system for proving that an object satis es a speci cation. The formalism includes the basic speci cation-building operations of the ASL speci cation language and is institution independent. 1 Introduction Modular structure is an important tool for organizing large and complex systems of interacting units. When a system is decomposed into self-contained modules with well-de ned interfaces, the number of possible interactions between parts of the system is greatly reduced. This makes it possible to understand each module in relative isolation from the other modules in the system. The application of modular structure to the organization of \dynamic" systems such as programs and machines is well known. Here, interactions between parts of a system involve transmission of data or physical contact between bits of metal. Its application to \static" systems such as algebraic speci cations is perhaps less obvious but just as important. Interactions here are more implicit and insidious, where axioms meant to specify one function can indirectly constrain the possible implementations of other functions as well. The rst algebraic speci cation language which provided the means to structure speci cations was CLEAR BG 80]. Since then the need for structure in speci cations has become universally recognized, and mechanisms for structuring speci cations appear in all modern algebraic speci cation languages including CIP-L Bau 85], ASL SW 83], Wir 86], ACT ONE EM 85] and the Larch Shared Language GHW 85]. An important structuring mechanism is parameterisation. This allows modules to be de ned in a generic fashion so that they may be applied in a variety of contexts which share some common characteristics. A parameterised program module F Gog 84] (an ML functor MacQ 86]) may be applied to y To appear in Acta Informatica. Department of Computer Science, University of Edinburgh, Edinburgh, UK. z Institute of Computer Science, Polish Academy of Sciences, Gdansk, Poland. x Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland. 1 any non-parameterised program module Aarg matching a given import interface Apar . The result is a non-parameterised program module F (Aarg ), a version of F in which the types and functions in Apar have been instantiated to the matching types and functions in Aarg . An example of a parameterised program module is a parser module which takes a lexical analyser module as argument. Similarly, a parameterised speci cation P may be applied to any non-parameterised speci cation SParg tting a certain signature par (or speci cation SPpar ) to yield a speci cation P (SParg ). A standard example is a speci cation Stack-of-X which takes a speci cation of stack elements and produces a speci cation of stacks containing those elements. In some algebraic speci cation frameworks, parameterisation is implicit in the sense that no distinction is made between parameterised and non-parameterised speci cations (see for example LOOK ETLZ 82], ASPIK Vo 85] and the uni ed algebra framework Mos 89a], Mos 89b]) but the idea is the same. The above discussion has dealt with two distinct classes: programs and speci cations. Appropriate parameterisation mechanisms give rise to two new (and distinct) classes: parameterised programs and parameterised speci cations. It is possible to specify parameterised programs, just as it is possible to specify non-parameterised programs. The result is not a parameterised speci cation; it is a nonparameterised speci cation of a parameterised program. In work on algebraic speci cation there has been a tendency to ignore this distinction and use one avour of parameterisation for both purposes. This has sometimes led to misunderstanding and confusion. In this paper, we argue that the distinction is important both for semantical reasons and because the two kinds of speci cations belong to di erent phases of program development: parameterised speci cations are used to structure requirements speci cations, while speci cations of parameterised programs are used to describe the modules which arise in the design of an implementation. The most natural way to structure a speci cation often re ects the way that an implementation would be structured. But this is not always the case, and then the lack of a distinction causes real problems. It is natural to consider what happens when parameterisation mechanisms are extended to the higher-order case in which parameterised objects are permitted as arguments and as results. This makes sense both for parameterised speci cations and for speci cations of parameterised programs. The consequences of such an extension are explored in this paper. It is shown that re-interpreting the concept of constructor implementation in ST 88b] in these terms leads to a natural extension to deal with implementations of speci cations of parameterised programs. This in turn supports an extension of the methodology for formal development of ML programs from speci cations presented in ST 89] to the case of higher-order ML functors. The paper is organized as follows. After some preliminary de nitions in Section 2, Section 3 surveys four of the approaches to parameterisation found in algebraic speci cation languages. This is not intended as an exhaustive overview of the literature on parameterisation; the four approaches discussed were found to be useful as a means of introducing the ideas in this paper, and many other related and important studies have been omitted (e.g. Ehr 82] and Gan 83], just to mention two). In Section 4, the similarities and di erences between these approaches are analysed. The distinction between parameterised speci cations and speci cations of parameterised programs is brought to light, and the consequences of this distinction are investigated. This part of the paper may be summarized by the following slogan: parameterised (program speci cation) 6= (parameterised program) speci cation In Sections 5 and 6, the technical and methodological consequences of extending parameterisation to the higher-order case are considered. Section 7 presents a speci cation formalism built on the institution-independent kernel speci cation language in ST 88a] which supports the speci cation of arbitrarily high-order parameterised programs, as well as extending the mechanism in ST 88a] for de ning rst-order parameterised speci cations to the higher-order case. This section is based on a 2 more extensive presentation of this formalism in ST 91a]. Finally, Section 8 contains conclusions and some ideas for future work. 2 Preliminaries Throughout the paper we assume that the reader is familiar with the basic concepts of logic and universal algebra. In particular we will freely use the notions of: algebraic many-sorted signature, usually denoted by , 0, 1, etc.; algebraic signature morphism : ! 0 (this yields the category of signatures SIGN ); -algebra; -homomorphism; -isomorphism; -equation; rst-order -sentence (the set of all -sentences will be denoted by Sen ( )); and satisfaction relation between -algebras and -sentences. These all have the usual de nitions (see e.g. ST 88a]) and a standard, hopefully selfexplanatory notation is used to write them down. We also make minor use of the pushout construction of category theory. For any signature , the class of all -algebras is denoted by Alg ( ). We will identify this with the category of -algebras and -homomorphisms whenever convenient. If : ! 0 is a signature morphism then : Alg ( 0) ! Alg ( ) is the reduct functor de ned in the usual way (the notation is sometimes used when is obvious). Now, given a signature morphism : ! 0 and functor F : Alg ( ) ! Alg ( 0), we say that F is (strongly) persistent along if for every algebra A 2 Alg ( ), F (A) = A. For any signature , by a -presentation we mean any set of -sentences. Any -presentation determines the class of its models, written ] , which consists of all -algebras that satisfy all the sentences in . By a -theory we mean any -presentation which is closed under semantical consequence, i.e., a set of -sentences is a -theory if all the sentences that hold in ] are in . The most basic assumption of work on algebraic speci cation is that software systems are modelled as algebras, abstracting away from the concrete details of algorithms and code and focussing on their functional behaviour. Roughly, the signature of the algebra gives the names of data types and of operations available to the user of the system, and the algebra itself gives the semantics of the particular realizations of these data types and operations de ned by the system. Consequently, to specify a software system viewed in this way means to give a signature ( x the abstract syntax available to the user) and de ne a class of algebras over this signature, that is, describe a class of admissible realizations of the system. One way to give a speci cation of a system is to present a list of axioms over a given signature and describe in this way the properties that the operations of the system are to satisfy. This view of a software-system speci cation as a -presentation (for an appropriate signature ) is perhaps the simplest possible, but has a number of disadvantages. Most notably, any speci cation of a real software system given in this style would comprise a very long, unstructured, and hence unmanageable list of axioms. To cope with this problem, a number of so-called speci cation languages have been designed, which allow speci cations to be built in a structured manner using a prede ned set of speci cationbuilding operations. According to the brief discussion above, the most essential feature of any such speci cation formalism is that every speci cation SP over a given signature (we will say that SP is a -speci cation) unambiguously determines the class of admissible realizations of the system being speci ed, i.e. a class of -algebras (sometimes referred to as models of the speci cation). Thus, any -speci cation SP denotes a class of -algebras S P ] 2 Pow (Alg ( ))1. A speci cation SP is called Pow (X ), for any class X , denotes the \class of all subclasses" of X . This raises obvious foundational di culties. We disregard these here, as they may be resolved in a number of standard ways. For example, for the purposes of this paper we could assume that algebras are built within an appropriate universal set, and deal with sets, rather than classes, of algebras. 1 3 consistent if it has at least one model, i.e. S P ] 6= ;. See ST 88a], ST 92] for a more extensive discussion of the semantics of speci cations. As a starting point for the presentation of speci cations in this paper, we recall here the simple yet powerful speci cation-building operations de ned in ST 88a] (with the slight di erence that signatures are regarded as speci cations in their own right here with impose on in place of h ; i). This was in turn based on the ASL speci cation language SW 83], Wir 86]. The main use of these operations is in examples where they should be more or less self-explanatory. The particular choice of speci cation-building operations is not important for the purposes of this paper. If is a signature, then is a -speci cation with the semantics: ] = Alg ( ) If SP is a -speci cation and is a set of -sentences, then impose on SP is a speci cation with the semantics: impose on SP ] = fA 2 S P ] j A j= g If SP is a -speci cation and : 0 ! is a signature morphism, then derive from SP by is a 0-speci cation with the semantics: derive from SP by ] = fA j A 2 S P ] g If SP is a -speci cation and : ! is a 0-speci cation with the semantics: 0 is a signature morphism, then translate SP by translate SP by ] = fA0 2 Alg ( 0) j A0 2 S P ] g If SP and SP 0 are -speci cations, then SP S P 0 is a -speci cation with the semantics: S P S P 0] = S P ] \ S P 0] If SP is a -speci cation and : 0 ! is a signature morphism, then minimal SP wrt is a -speci cation with the semantics: minimal SP wrt ] = fA 2 S P ] j A is minimal in Alg ( ) w.r.t. g2 where a -algebra A is minimal w.r.t. if it has no non-trivial subalgebra with an isomorphic -reduct (cf. ST 88a]). If SP is a -speci cation, then iso-close SP is a -speci cation with the semantics: iso-close SP ] = fA 2 Alg ( ) j A is isomorphic to B for some B 2 S P ] g If SP is a -speci cation, : ! 0 is a signature morphism and 0 is a set of 0-sentences, then abstract SP wrt 0 via is a -speci cation with the semantics: abstract SP wrt 0 via ] = fA 2 Alg ( ) j A B for some B 2 S P ] g where A B means that A is observationally equivalent to B w.r.t. 0 via (see ST 87], ST88a] for details). 0 0 2 This is slightly di erent from the de nition in ST 88a]. 4 The above de nitions were given in ST 88a] in the framework of an arbitrary institution GB 84]. This means that the speci cation-building operations de ned above are actually independent of the underlying logical system, that is, of the particular de nitions of the basic notions of signature, algebra, sentence and satisfaction relation. In this paper it will be convenient to use some other speci cation-building operations de ned in the standard framework of rst-order logic, as follows: 0 If SP is a -speci cation and SP 0 is a 0-speci cation, then SP + SP 0 is a ( )-speci cation with the semantics: S P + SP 0] = fA 2 Alg ( 0 ) j A 2 S P ] and A 0 2 S P 0] g (this is expressible using union and translate as de ned above, see ST 88a]). If SP is a -speci cation, S is a set of sort names, is a set of ranked operation names such that adding S and to yields a well-formed signature 0, and 0 is a set of 0-sentences, then enrich SP by sorts S opns axioms 0 is a 0-speci cation with the semantics: enrich SP by sorts S opns axioms 0] = fA 2 Alg ( 0) j A 2 S P ] and A j= 0g (this is expressible using translate and impose as de ned above, see ST 88a]). If SP is a -speci cation and S is a set of sort names in , then reachable SP on S is a -speci cation with the semantics: reachable SP on S ] = fA 2 S P ] j A is generated on S g where A is said to be generated on S if it has no proper subalgebra having the same carriers of sorts not in S (this is expressible using minimal as de ned above, see ST 88a]). For example we can now de ne: Bool =def reachable sorts bool opns true; false : ! bool axioms true 6= false on fboolg Nat =def ::: ::: reachable enrich Bool by sorts opns nat zero : ! nat succ : nat ! nat > : nat nat ! bool axioms 8n : nat: succ(n) > zero = true on fnatg ::: Note that at the semantical level, each of the speci cation-building operations introduced above is a function mapping classes of algebras to classes of algebras. We will assume that when viewed this 5 ::: way, all speci cation-building operations are monotone w.r.t. the inclusion ordering on classes. This is indeed the case for all the above operations. If SP is a -speci cation and SP 0 is a 0-speci cation, then a speci cation morphism from SP to SP 0, : SP ! SP 0, is a signature morphism : ! 0 such that for all A0 2 S P 0] , A0 2 S P ] . This yields the category of speci cations SPEC (with composition and identities inherited from the category of signatures SIGN ). SPEC is co-complete, with colimits in SPEC determined by colimits in SIGN (cf. GB 84], ST 88a]). Note that this de nition of speci cation morphism works for any speci cation formalism with a semantics in the style presented above. 3 Overview of parameterisation mechanisms A speci cation language provides a certain number of speci cation-building operations such as those de ned above. As we have mentioned, such operations may be viewed as functions mapping speci cations to speci cations. More complex functions of this type may be de ned as combinations of the elementary speci cation-building operations provided. We can use -abstraction to write such functions down, where the semantics of application is given by -conversion. This is the approach adopted in ASL SW 83], Wir 86]; the particular de nition below is taken from ST 88a] with a minor syntactic modi cation (viz., the use of Spec ( ) to conform with conventions to be introduced later). De nition 3.1 An ASL-style parameterised speci cation has the form X :Spec ( par): SPres X ] where par is a signature and SPres X ] is a res -speci cation which may contain one or more uses of X as a par -speci cation. The result of applying such a parameterised speci cation to a par -speci cation SParg is de ned as follows: ( X :Spec ( par): SPres X ])(SParg ) =def SPres S Parg =X ] where SPres S Parg =X ] is SPres with all occurrences of X replaced by SParg . This naturally extends to higher-order parameterised speci cations in the standard way. Recursion is also no problem since all speci cation-building operations are monotonic with respect to the inclusion of model classes. A characteristic feature of the speci cation-building operations de ned in Section 2 and in ST 88a] is that the signature of SPres S Parg =X ] is not dependent on SParg : SPres S Parg =X ] is a res -speci cation for any par -speci cation SParg . Thus a parameterised speci cation X :Spec ( par ): SPres X ] describes a function mapping par -speci cations to res -speci cations. This function is only de ned for speci cations over the indicated parameter signature par . In the framework of ST 88a], it is possible to apply a parameterised speci cation X :Spec ( par ): SPres X ] to a arg -speci cation SParg where arg par , but only by rst applying derive to SParg (via the inclusion morphism : par ,! arg ); the same trick works for any SParg where there is a signature morphism : par ! arg . The part of SParg which is thereby \forgotten" does not reappear in the result of the application. A di erent approach is taken in CLEAR BG 80], where parameterised speci cations are used to uniformly enrich given argument speci cations. In this approach, everything which is in the argument speci cation carries through to the overall result. This is achieved by making the \ tting" of the argument speci cation to the indicated parameter signature an explicit part of the argument-passing mechanism. De nition 3.2 A CLEAR-style parameterised speci cation is a speci cation morphism P : SPpar ! SPres , where SPpar is a par -speci cation and SPres is a res -speci cation. The overall result of applying such a parameterised speci cation to a arg -speci cation SParg via a speci cation morphism 0 : SPpar ! SParg (a so-called tting morphism) is de ned as the speci cation SPres where 6 S Parg 6 0 - SPres 6 SPpar P - SPres is a pushout in the category of speci cations SPEC. 0 S Pres may be de ned more explicitly as follows: 0 b SPres =def (translate SParg by P ) (translate SPres by b ) b where P and b are given by the following pushout diagram in the category of signatures SIGN : arg 6 b P - 0 res 6 b par P - res This still de nes a function taking speci cations to speci cations, but the signatures of the argument and of the overall result speci cations are not xed. Further di erences with respect to ASL-style parameterisation are that the argument speci cation is required to \semantically" t the parameter speci cation SPpar rather than just to \syntactically" t the parameter signature par as before, and that the argument speci cation is always explicitly included in the overall result speci cation. ACT ONE EM 85] adopts a similar style of parameterisation to that of CLEAR except that it has an additional layer of semantics. Namely, in addition to the way in which application of a parameterised speci cation to an argument speci cation builds an overall result speci cation as above, a parameterised speci cation describes a functor mapping individual models of the parameter speci cation to models of the result speci cation. De nition 3.3 An ACT ONE-style parameterised speci cation and application of such a parameterised speci cation to an argument speci cation are de ned exactly as for CLEAR-style parameterised speci cations, except that the only speci cations considered are presentations with equational axioms. The model-level semantics of a parameterised speci cation P : SPpar ! SPres is the free functor FP : S Ppar ] ! S Pres ] (the left adjoint to the P -reduct functor P : S Pres ] ! S Ppar] ). In ACT ONE, an important issue is the compatibility of the speci cation-level semantics with the model-level semantics, where the model-level semantics of an unparameterised speci cation is the class of its initial models. It turns out that everything works out ne when the free functor de ned by a parameterised speci cation is persistent. In this case, for any argument speci cation SParg and tting 7 0 morphism : SPpar ! SParg , FP : S Ppar ] ! S Pres ] lifts to a functor FP : S Parg ] ! S Pres ] (via b the amalgamation lemma) which is free with respect to P and so maps the initial models of SParg b 0 to the initial models of SPres . The model-level semantics of ACT ONE-style parameterisation has a completely di erent avour from the previous parameterisation mechanisms. ACT ONE parameterised speci cations are not purely construed as speci cation-building operations but also as tools to construct models of the overall results out of models of the arguments. This is very much like module parameterisation mechanisms in modular programming languages such as Standard ML MacQ 86], which was the starting point for work on the Extended ML speci cation language ST 85], ST 89], San 91], ST 91b]. Such modularisation mechanisms provide the means to structure programs \in the large" so that programs may be decomposed into a number of (possibly generic) self-contained units with well-de ned interfaces Gog 84]. The Standard ML programming language comprises two layers: an essentially functional programming language, and a language for de ning program units (structures), interfaces (signatures) and parameterised program units (functors). Simplifying somewhat, we can think of structures as algebras, ML signatures as algebraic signatures, and functors as parametric algebras, i.e. functions mapping algebras to algebras (cf. OBSCURE LL 88] where these are called algebra modules). Extended ML provides a means of specifying such parametric algebras (cf. the notion of cell in Sch 87]). Extended ML functor speci cations are like Standard ML functors except that the result of applying the functor to an argument algebra is (loosely) speci ed rather than de ned explicitly by means of code. To simplify the presentation, we consider only those functors in which the result includes the parameter. De nition 3.4 An Extended ML functor speci cation has the form functor F (X : SPpar ) : SPres where SPpar is a par -speci cation and SPres is a res -speci cation with par res . Its semantics is a function F which to any algebra A 2 S Ppar ] assigns a res -speci cation F (A) with semantics de ned as follows: F (A)]] = fB 2 S Pres ] j B par = Ag A Standard ML functor which maps par -algebras to res -algebras satis es this speci cation i for each algebra A 2 S Ppar ] it yields an algebra in F (A)]]. The semantics of an Extended ML functor speci cation F as above extends pointwise to any argument par -speci cation SParg such that S Parg ] S Ppar ] : F (SParg ) is a res -speci cation with semantics de ned as follows: F (SParg )]] = f F (A)]] j A 2 S Parg ] g Note that the function described by an Extended ML functor speci cation is persistent by de nition, in the sense that any algebra B in F (A)]] inherits an unmodi ed copy of A. For Standard ML functors, where both the argument and the body of the functor are de ned by Standard ML code, this embodies the fact that the code of the argument cannot be modi ed by adding the additional code in the body. This constraint is retained when generalising to speci cations of Standard ML functors as in Extended ML. In Extended ML, however, this may lead to inconsistency since the axioms in the result speci cation may impose new requirements on the argument: for some algebras A 2 S Ppar ] , F (A)]] may be empty, as happens when the requirements imposed in SPres are inconsistent with the particular realization of SPpar given by A. There will then be no Standard ML functor which satis es the speci cation since such a functor must produce a result for all algebras which satisfy SPpar . In this section we described a number of di erent parameterisation mechanisms appearing in speci cation languages. One obvious di erence between them concerns the technicalities of parameter passing, which in ASL is based on -reduction in a -calculus style, while CLEAR and ACT ONE use 8 a pushout-based approach. Advocates of the pushout approach argue for its convenience, since for an arbitrarily large argument the overall result always includes the whole argument. This is not the case in ASL, as discussed above. The pushout approach seems fully justi ed in a formalism used to gradually construct a single speci cation by successively adding pieces. The idea is to incorporate in this speci cation all potentially useful components, as otherwise they may be lost. However, a real speci cation language will incorporate an environment of named speci cations, with explicit scoping mechanisms like those in declarative programming languages. Once a speci cation is introduced into the environment, it remains there and all of its components are permanently accessible. Whichever parameterisation mechanism is used, there is no danger that some components of an actual parameter will inadvertently become unavailable. If needed, they can always be taken from the environment, subject only to the constraints of the type system and the scoping mechanisms. Speci cation languages like Extended ML are designed to be su ciently permissive to allow this (cf. Tar 92]). Such di erences will to a large extent be disregarded in this paper; although they are of great importance for practical purposes, the di erence is a matter of taste and convenience rather than of a more fundamental nature. 4 Parameterised speci cations vs. speci cations of parametric algebras 4.1 Concepts and semantic objects An essential di erence between the parameterisation approaches presented in Section 3 may best be seen if we compare the ASL-style and Extended ML-style parameterisation mechanisms. ASL-style parameterised speci cations are de ned entirely on the level of speci cations, without any reference to the algebras which speci cations are used to describe. Thus, they accept speci cations as arguments and yield speci cations as results. De ning the semantics of Extended ML functor speci cations at this level was possible only via the more basic level of algebras: an Extended ML functor speci cation describes a function taking single algebras to classes of algebras, which is viewed as a de nition of a class of Standard ML functors. The pointwise extension to speci cations is a posteriori, and in fact plays no part in the Extended ML program development methodology proposed in ST 89], ST 91b]. CLEAR-style parameterised speci cations are similar in this respect to ASL-style parameterisation, while ACT ONE-style parameterisation has elements of both embodied in its two levels of semantics. This distinction seems fundamental as it re ects the role which both kinds of speci cations play in the program development process. There are two kinds of entities involved in the process of developing a software system from a speci cation. On one hand we have software systems, modelled as algebras. On the other hand we have speci cations which describe classes of algebras. Both software systems and speci cations may (and should) be presented in a structured way, using mechanisms such as parameterisation. This gives rise to both parametric (or generic) software systems, and parameterised speci cations. It is easy to confuse two distinct notions: speci cations of parametric software systems, and parameterised speci cations of software systems. The rst is a (non-parameterised) speci cation of a parametric algebra. Extended ML-style functor speci cations are of this kind. The second is a parameterised speci cation of a (non-parametric) algebra. ASL-style and CLEAR-style parameterised speci cations are of this kind. Of course, it is possible to combine these two notions to obtain (for example) parameterised speci cations of parametric algebras, etc. A technical consequence of the above considerations is that the semantic objects modelling parameterised speci cations and speci cations of parametric algebras are quite di erent. 9 result signature De nition 4.1 The denotation of a parameterised speci cation P with parameter signature res is a monotone function par and P ] : Pow (Alg ( par )) ! Pow (Alg ( res )) mapping classes of par -algebras to classes of res-algebras. The collection of all such functions is called Spec ( par ) ! Spec ( res ); we write P : Spec ( par ) ! Spec ( res) to indicate the \type" of P . We will use the notation of ASL to de ne parameterised speci cations. The de nition of the application of a parameterised speci cation P (De nition 3.1) yields a monotone function P ] as above (cf. Section 7.2). When needed, we will use the same notation with a parameter (requirement) speci cation instead of just a parameter signature (cf. Section 7). The denotation of a parameterised speci cation P with parameter speci cation SPpar and result signature res is a monotone function P ] : Pow ( SPpar ] ) ! Pow (Alg ( res )) mapping classes of SPpar-models to classes of res -algebras. De nition 4.2 The denotation of a speci cation Q of res -algebras parameterised by par -algebras is a class Q] 2 Pow (Alg ( par ) ! Alg ( res )) of functions mapping par -algebras to res -algebras. The collection of all such functions is called Spec ( par ! res ); we write Q : Spec ( par ! res ) to indicate the \type" of Q. We will use a notation like A: par : SP A] for speci cations of parametric algebras. A: par : SP A]]] is the class of functions F which map any par -algebra A to an algebra F (A) 2 S P A]]]. Here, SP A] is a speci cation in which A stands for a par-algebra. A can be used in SP via a new speci cation-building operation which turns algebras into speci cations: if A is a -algebra then fAg is a -speci cation having A as its only model. We can readily generalise this and use an arbitrary speci cation rather than a signature to de ne the class of algebras over which the \parameter" A ranges (cf. Section 7). The denotation of a speci cation Q of res -algebras parameterised by SPpar -models is a class Q] 2 Pow ( SPpar] ! Alg ( res)) of functions mapping SPpar -models to res -algebras. Extended ML functor speci cations may be modelled as speci cations of parametric algebras: functor F (X : SPpar) : SPres speci es the class of Standard ML functors F which are parametric algebras in the class de ned by X :SPpar : SPres . The following two simple examples illustrate the notions introduced above. Other examples will follow in later sections. Example 4.3 Let Key =def enrich Nat by sorts key opns hash : key ! nat 10 where Nat is as de ned in Section 2, and let HashTable1 =def X : Spec (Key): enrich X by sorts opns array empty : ! array used : nat array ! bool put : nat key array ! array get : nat array ! key add : key array ! array putnear : nat key array ! array present : key array ! bool searchnear : nat key array ! bool axioms used(i; empty) = false : : : (axioms for arrays) : : : add(k; a) = putnear(hash(k); k; a) used(i; a) = false ) putnear(i; k; a) = put(i; k; a) used(i; a) = true ^ get(hash(k); a) = k ) putnear(i; k; a) = a used(i; a) = true ^ get(hash(k); a) 6= k ) putnear(i; k; a) = putnear(i + 1; k; a) present(k; a) = searchnear(hash(k); k; a) used(i; a) = false ) searchnear(i; k; a) = false used(i; a) = true ^ get(hash(k); a) = k ) searchnear(i; k; a) = true used(i; a) = true ^ get(hash(k); a) 6= k ) searchnear(i; k; a) = searchnear(i + 1; k; a) (Each axiom is implicitly universally quanti ed over all its free variables; this convention will be used in examples throughout the rest of this paper.) HashTable1 is a parameterised speci cation. Given a speci cation SP describing a particular choice for keys and perhaps constraining hash in some fashion (e.g. to have a particular subset of the natural numbers as its range), HashTable1 (SP ) is a speci cation of hash tables containing such keys and using such a hash function. For instance, let String =def enrich Nat by sorts string opns nil : ! string a : ! string b : ! string c : ! string : string string ! string hash : string ! nat axioms s nil = s nil s = s s (t v) = (s t) v hash(nil) = 0 Let Key and String be the signatures of Key and String respectively, and let : 11 Key ! String be the obvious signature morphism (mapping key to string and leaving the rest of the signature of Key unchanged). Then HashString =def HashTable1(derive from String by ) speci es hash tables containing strings, with the hash function constrained so that the empty string is hashed into position 0 of the table. Note that adding further axioms to String which constrain its class of models and then repeating the construction of HashString with this new version of String would yield a speci cation with fewer models than HashString as above. This demonstrates the monotonicity of the function which HashTable denotes. The above example can be made slightly more realistic by adding a use of derive to the body of HashTable1 to hide some operations (e.g. putnear ) and to change the name of the sort array to hashtable. Example 4.4 Let HashTable2 =def A : Key: enrich fAg by sorts opns array empty : ! array used : nat array ! bool : : : (as in the previous example) : : : axioms used(i; empty) = false : : : (as in the previous example) : : : where Key is as in Example 4.3. HashTable2 is a speci cation of a parametric algebra. If H is in the class de ned by HashTable2 , then H is a function mapping algebras to algebras. For any algebra A satisfying the speci cation Key, H (A) is an algebra which realizes hash tables containing the keys in A and using the hash function in A. H (A) is required to satisfy the axioms in the body of HashTable2 for any A satisfying Key, so any H satisfying HashTable2 will be a universally applicable parameterised implementation of hash tables, in the sense that it is required to exhibit correct behaviour for any choice of keys and any choice of hash function over those keys. The above two examples illustrate the essential di erence of intention underlying (instantiated) parameterised speci cations vs. speci cations of parametric algebras. To realize HashString (Example 4.3), the implementor must provide an implementation of hash tables for a hash function of his/her choice (subject only to the constraint that hash (nil ) = 0). To realize HashTable2 (Example 4.4), the implementor must provide an implementation of hash tables which works for any hash function, since the hash function will be supplied later as an argument. There is a natural connection between the semantic domains of parameterised speci cations and speci cations of parametric algebras having the same parameter and result signatures. This relationship is captured as follows. (The technicalities below do not depend on the fact that we deal with the meanings of speci cations here; we just apply some standard ideas of lattice theory Bir 48] to our speci c concepts.) Note that all of the following extends to the case where we have a parameter speci cation instead of just a parameter signature. Recall that Spec ( par ) ! Spec ( res ) stands for the function space Pow (Alg ( par )) ! Pow (Alg ( res )) with elements P (these are monotonic functions corresponding to the denotations of parameterised 12 4.2 The Galois connection speci cations P ). Similarly, Spec ( par ! res ) stands for Pow (Alg ( par) ! Alg ( res)) with elements Q (these correspond to the denotations of speci cations Q of parametric algebras). As usual, in examples we will avoid stressing the distinction between a (parameterised) speci cation and its denotation, and use the same name to refer to both. De nition 4.5 For any P 2 Spec ( par ) ! Spec ( res ), let P ] 2 Spec ( par ! res ) be de ned by P ] = fF : Alg ( For any Q 2 Spec ( for any class C of par par ) ! Alg ( res ) j for all A 2 Alg ( par ), F (A) 2 P (fAg)g: ! res ), let Qy 2 Spec ( par ) ! Spec ( res ) be de ned by Qy(C ) = fF (A) j F 2 Q; A 2 C g par -algebras. HashTable2 in Example 4.4. We have: Example 4.6 Recall the parameterised speci cation HashTable1 in Example 4.3 and the speci cation HashTable1] = HashTable2 HashTable2y = HashTable1 Proposition 4.7 1. Spec ( par ! res ) forms a complete lattice with the set inclusion ordering. 2. Spec ( par ) ! Spec ( res ) forms a complete lattice with the natural extension of the set inclusion ordering on Spec ( res) = Pow (Alg ( res )): for P1; P2 2 Spec ( par) ! Spec ( res ), P1 P2 i for all C Alg ( par), P1(C ) P2(C ). ! res), if Q1 Q2 then Qy Qy . 1 2 ] ] 4. For P1; P2 2 Spec ( par ) ! Spec ( res), if P1 P2 then P1 P2. 5. For Q 2 Spec ( par ! res), Q (Qy)]. 6. For P 2 Spec ( par ) ! Spec ( res ), P (P ])y. par 3. For Q1; Q2 2 Spec ( Proof Immediate from the de nitions, but note that 6 relies on the monotonicity of P . Corollary 4.8 The maps ( )] and ( )y de ned above are isomorphisms between the sublattices of Spec ( par Thus we have de ned a Galois connection Bir 48]. and Spec ( par ) ! Spec ( res) consisting of their closed elements, i.e. of parameterised speci cations of the form (P ])y and of speci cations of parametric algebras of the form (Qy)], respectively. res ) ! par ), the function F : Alg ( is an element of Q as well. A 2 Alg ( De nition 4.9 Q 2 Spec ( par ! res ) is called regular par ) ! Alg ( res ) de if for every family of functions FA 2 Q, ned by F (A) = FA(A) for A 2 Alg ( par ) 13 (), ): By Proposition 4.7.5. (), ): Consider any F : Alg ( par) ! Alg ( res ) such that F (A) 2 Qy(fAg) for all A 2 Alg ( par). The de nition of Qy implies now that for all A 2 Alg ( par), there is FA 2 Q such that F (A) = FA(A). Thus F 2 Q since Q is regular. Proposition 4.10 Q 2 Spec ( par ! res ) is regular i it is closed, i.e. i Q = (Qy)]. Proof ((): Directly from the de nition; for all P 2 Spec ( par ) ! Spec ( res ), P ] is regular. P (C ) = fP (fAg) j A 2 C g. Fact 4.12 If P 2 Spec ( par) ! Spec ( res ) is not additive then P (P ])y. De nition 4.13 P 2 Spec ( par ) ! Spec ( res ) is called globally inconsistent if P (C ) = ; for all C Alg ( par ). De nition 4.14 P 2 Spec ( par) ! Spec ( res ) is said to preserve consistency if P (C ) = ; for all 6 non-empty C Alg ( par ). (P ])y is globally inconsistent. De nition 4.11 P 2 Spec ( S par ) ! Spec ( res ) is called additive if for every class C Alg ( par ), Fact 4.15 If P 2 Spec ( par ) ! Spec ( res ) does not preserve consistency then P ] is inconsistent and either Q = ;, and then Qy is globally inconsistent, or Q 6= ;, and then Qy preserves consistency. ((): If P is globally inconsistent, then P ] = ; and so P = (P ])y trivially. Otherwise, by additivity of P and of (P ])y (the latter follows from the proof of the opposite implication, above) and by Proposition 4.7.6, it is enough to show that P (fAg) (P ])y(fAg). For all A0 2 Alg ( par), P (fA0g) 6= ;, since P preserves consistency. Consequently, for all B 2 P (fAg), there is F 2 P ] such that F (A) = B , and thus B 2 (P ])y(fAg). Proposition 4.16 P 2 Spec ( par ) ! Spec ( res ) is closed, i.e. P = (P ])y, i either P is globally inconsistent, or P is additive and preserves consistency. Proof ()): Directly from the de nition. For all Q 2 Spec ( par ! res ), Qy is additive. Moreover, Corollary 4.17 There is a 1-1 correspondence between consistent regular speci cations of parametric algebras and additive parameterised speci cations which preserve consistency. consistency. The speci cation HashTable2 in Example 4.4 is regular and consistent. In fact, HashTable1 and HashTable2 are in the correspondence mentioned in Corollary 4.17 (cf. Example 4.6). Example 4.18 The parameterised speci cation HashTable1 in Example 4.3 is additive and preserves Some explanation of the properties embodied in the above technicalities will make their signi cance clearer. Q 2 Spec ( par ! res ) is regular i it is a Cartesian product of a family of classes of algebras indexed by par -algebras. This is a natural condition which is met by all the speci cations we are going to write (and indeed by all speci cations expressible in Extended ML). The -notation used above and later formally introduced in Section 7 for de ning speci cations of parametric algebras has a semantics which may be decomposed into two stages. Consider A: par : SP A], where SP A] is a res -speci cation. First, this directly de nes a function F : Alg ( par) ! Pow (Alg ( res )) which maps any par -algebra A to the class of algebras S P A]]]. This is then used to determine a class of functions A2Alg ( par )F (A) 2 Spec ( par ! res ) ( is used here as the Cartesian product symbol) which is the meaning of the speci cation A: par : SP A]. Clearly, any speci cation de ned in this way is regular. Violating regularity would require use of speci cation mechanisms which constrain 14 the instantiation of a parametric algebra on an argument by relating it to the instantiation of this parametric algebra on other arguments. For example, the \stability" of Standard ML functors (see Sch 87], ST 89], ST 92]) is such a constraint. Thus, if a speci cation language provided a way to require stability of parametric algebras (Standard ML functors) it might allow non-regular classes of functors to be speci ed. With regard to additivity of parameterised speci cations, we have assumed that all speci cationbuilding operations (and therefore also parameterised speci cations) are monotonic on model classes. This ensures that P (C ) SfP (fAg) j A 2 C g for every P 2 Spec ( par ) ! Spec ( res ) and C Alg ( par ). Thus, the only way for a parameterised speci cation to be non-additive is for the opposite inclusion to fail. This may happen if it operates on the class of models of its argument as a whole rather than \pointwise". The following example of an ASL parameterised speci cation shows the di erence. Example 4.19 Let ab =def sorts s opns a :! s b :! s and c =def sorts s opns c :! s with signature morphisms ca; cb : c ! ab where ca(s) = cb(s) = s, ca(c) = a and cb(c) = b. Now, consider the ASL parameterised speci cation P =def X :Spec ( ab ): (derive from X by ca) (derive from X by cb ): P is not additive. Consider two ab -algebras, A; B with As = Bs = f0; 1g and aA = 0; bA = 1; aB = 1; bB = 0. It is easy to see that P ] (fAg) = P ] (fB g) = ; while P ] (fA; B g) = fC; Dg where Cs = Ds = f0; 1g, cC = 0 and cD = 1. It is interesting to observe that each of the ASL speci cation-building operations used in this example (and all those de ned in Section 2) are additive. Paradoxically, it was nevertheless possible to use them to form a non-additive parameterised speci cation. The reason is that there is a hidden non-additive operation built into the notation, namely the \diagonalisation" function which allows an argument to be used repeatedly as in X :Spec ( ): (: : :X : : :X : : :). It is also possible to imagine full- edged speci cation-building operations which are non-additive. For example, one might like to de ne a class of algebras by rst specifying the boundaries of the admissible behaviour and then applying a speci cation-building operation which lls in all those algebras which exhibit behaviour within these boundaries. Such an operation would be non-additive. Example 4.19 is also an example of a parameterised speci cation which does not preserve consistency (e.g. P ] (fAg) = ;) without being globally inconsistent (e.g. P ] (fA; B g) 6= ;). Among the speci cation-building operations de ned in Section 2, derive, translate (with respect to injective signature morphisms), iso-close and abstract preserve consistency. A parameterised speci cation preserves consistency i it is in principle realizable by a parametric algebra: for every model of the argument speci cation there is a model of the result speci cation. The use operation in the PLUSS speci cation language is explicitly designed to have this property, as described in Bid 88] (cf. GM 88]). 15 Example 4.20 Let Sort =def Ord be the signature obtained by adding a sort elem and an operation lt : elem elem ! bool to the signature of the speci cation Bool de ned in Section 2. Then, let X : Spec ( enrich X by sorts opns Ord ): list nil : ! list cons : elem list ! list is-in : elem list ! bool is-sorted : list ! bool sort : list ! list axioms is-in(x; nil) = false is-in(x; cons(x; l)) = true x 6= y ) is-in(x; cons(y; l)) = is-in(x; l) is-sorted(nil) = true is-sorted(cons(x; l)) = true , (8y : elem: is-in(y; l) = true ) lt(y; x) = false) ^ is-sorted(l) = true is-in(x; l) = is-in(x; sort(l)) is-sorted(sort(l)) = true Sort is a parameterised speci cation. Given a speci cation of data elements with a binary relation, it builds a speci cation of lists of these elements together with an operation which sorts lists with respect to the given relation. Here are some speci cations which constitute admissible arguments for Sort : Ord =def enrich Bool by sorts elem opns lt : elem elem ! bool axioms lt(x; y) = true ) lt(y; x) = false lt(x; y) = true ^ lt(y; z) = true ) lt(x; z) = true This speci es a strict (i.e. irre exive) partial ordering. Then, Sort (Ord ) is a speci cation of topological sorting. LOrd =def enrich Ord by axioms lt(x; y) = false ^ lt(y; x) = false ) x = y This speci es a total (linear) ordering. Then, Sort (LOrd ) is a speci cation of ordinary sorting, except that the sort operation is permitted to remove duplicate elements. Tot =def enrich Bool by sorts elem opns lt : elem elem ! bool axioms lt(x; y) = true 9x; y : elem: x 6= y This speci es a \total" relation with at least two di erent values of sort elem. Then, Sort (Tot ) is inconsistent! (Suppose a and b are two di erent values of sort elem ; then according to the axioms for is-in and the penultimate axiom in the body of Sort, we have that sort (cons (a; cons (b; nil ))) is either cons (a; cons (b; nil )) or cons (b; cons (a; nil )), or a list with duplicates for which the same argument applies. Since the rst axiom of Tot requires that lt (a; b) = lt (b; a) = true , we have 16 is-sorted(cons (a; cons (b; nil ))) = false and is-sorted(cons (b; cons (a; nil ))) = false , so neither of these two values satis es the last axiom of Tot.) Thus Sort does not preserve consistency although it is not globally inconsistent. Let SP Sort X ] denote the body of Sort. Then Sort ] may be given explicitly as follows: Sort] = A: Ord : SPSort fAg] Since Sort does not preserve consistency, Sort ] is inconsistent and (Sort ])y is globally inconsistent (Fact 4.15). Thus Sort (Sort ])y. Intuitively, Sort ] is a speci cation of a parametric algebra which for any set of elements with a binary relation builds an algebra of lists of elements together with, among others, an operation to sort lists with respect to the relation. Unfortunately, for non-antisymmetric binary relations a sorting operation satisfying the axioms in Sort cannot exist, and so Sort ] cannot be implemented (Sort ] is inconsistent). We can modify Sort, restricting the range of admissible parameters so that the binary relation lt is forced to be a (strict) partial ordering: d Sort =def X :Spec (Ord): SPSort X ] d Sort] = A:Spec (Ord): SPSort fAg] d It is easy to check that on the domain determined by Ord as above, Sort preserves consistency and is ]y d additive, and so (Proposition 4.16) Sort = (Sort ) . Then we have 4.3 Methodological consequences The upshot of the above deliberations is that there are two distinct things: parameterised speci cations, and speci cations of parametric algebras. Corollary 4.17 characterises the proper subclasses of these two classes which essentially coincide. The properties of additivity and preserving consistency characterise the class of parameterised speci cations which can be adequately viewed as consistent speci cations of parametric algebras. Regularity of a speci cation of a parametric algebra ensures that it can be regarded as a parameterised speci cation. This does not mean that these properties are to be viewed as requirements to be imposed on all parameterised speci cations and speci cations of parametric algebras. We believe there is a role for both non-additive and non-consistency-preserving parameterised speci cations in the process of software development. Non-regular speci cations of parametric algebras are useful as well, although in Extended ML ST 89], ST 91b] we decided to introduce the only potential non-regular speci cation-building operation (the requirement of stability) at a di erent level. Corollary 4.17 is not meant to suggest either that the subclasses of speci cations having these properties should be identi ed. There is an important methodological distinction between parameterised speci cations and speci cations of parametric algebras. Parameterised speci cations are tools for building requirements speci cations in a structured way. The structure which is thereby introduced makes the requirements speci cation easier to understand, reason about and use; it is not meant to impose any restriction on the structure of the eventual implementation. In contrast, speci cations of parametric algebras are used in the process of designing an implementation. They are introduced for the express purpose of imposing structure on the desired implementation, breaking the problem into self-contained chunks which may be tackled independently. Once the job is completed, the result is a collection of self-contained modules with precisely-speci ed interfaces, all of which may later be reused in other systems. 17 The structure of the requirements speci cation may suggest a possible way of decomposing the speci ed task into subtasks. However, if the parameterised speci cations involved do not preserve consistency then it will not be possible to provide implementations of the corresponding subtasks (Fact 4.15). In this case it is necessary to seek an alternative way of decomposing the problem. Less dangerously, if the parameterised speci cations involved are not additive then imposing the structure of the speci cation on the solution may exclude some of the models of the original requirements speci cation (Fact 4.12). In this case, it may be useful to seek an alternative way of decomposing the problem which admits more, possibly better, solutions. Even when all the parameterised speci cations involved are both additive and preserve consistency, the structure of the requirements speci cation may not be the best structure for the implementation (for example, for e ciency reasons) and so the implementation team should not be compelled to use it. Thus, in any case, the designer should not be forbidden from seeking an alternative way of decomposing the problem; the need to eventually obtain an algebra which realizes the requirements speci cation should be the only constraint. See FJ 90] for a similar conclusion supported by evidence from a practical example. Example 4.21 The following simple example illustrates some of the points made above. Let Bunch =def reachable enrich Nat by sorts elem; bunch opns empty : ! bunch add : elem bunch ! bunch removeone : elem bunch ! bunch count : elem bunch ! nat axioms count(a; empty) = 0 count(a; add(a; B )) > 0 = true a 6= b ) count(a; add(b; B )) = count(a; B ) count(a; B ) = 0 ) count(a; removeone(a; B )) = 0 count(a; B ) 6= 0 ) count(a; removeone(a; B )) = count(a; B ) ? 1 a 6= b ) count(b; removeone(a; B )) = count(b; B ) on fbunchg Bunch is a generalisation of nite sets, bags, lists, etc. The intention is that count counts the number of occurrences of a given element in a bunch and removeone removes one occurrence of an element from a bunch. The operation add is not constrained except that adding an element to a bunch does not change the number of occurrences of other elements in the bunch, and leaves in the bunch at least one occurrence of the indicated element. In a realization of bunches using bags or lists, add would add one occurrence of the indicated element. There are also realizations of bunches in which add would add more than one occurrence of the element, and even realizations in which, under some 18 circumstances, add would decrease the number of occurrences of the \added" element (as long as it does not remove them all). Set =def reachable add : elem bunch ! bunch removeone : elem bunch ! bunch count : elem bunch ! nat axioms add(a; add(b; B )) = add(b; add(a; B )) add(a; add(a; B )) = add(a; B ) count(a; empty) = 0 count(a; add(a; B )) = 1 a 6= b ) count(a; add(b; B )) = count(a; B ) count(a; B ) = 0 ) removeone(a; B ) = B count(a; B ) = 0 ) removeone(a; add(a; B )) = B on fbunchg Set is a specialization of Bunch (in the sense that Set ] Bunch ] ) in which each element occurs at most once in a bunch (so count is never greater than 1) and add is required to be idempotent and enrich Nat by sorts elem; bunch opns empty : ! bunch commutative. Delete =def X :Spec (Bunch): enrich X an operation delete which removes all occurrences of the indicated element from a bunch. Note that Delete is additive and preserves consistency. The parameterised speci cation Delete may be applied to the speci cation Bunch: BunchDelete =def Delete(Bunch) Suppose that BunchDelete is the requirements speci cation we are to implement. As a requirements speci cation, this conveys exactly the same information as the following equivalent non-parameterised speci cation: a 6= b ) count(a; delete(b; B )) = count(a; B ) The parameterised speci cation Delete takes any speci cation SP with S P ] Bunch ] and adds by opns delete : elem bunch ! bunch axioms count(a; delete(a; B )) = 0 enrich reachable enrich Nat by sorts elem; bunch opns empty : ! bunch axioms : : : on fbunchg by opns delete : elem bunch ! bunch axioms : : : 19 add : elem bunch ! bunch removeone : elem bunch ! bunch count : elem bunch ! nat The requirements speci cation BunchDelete is correctly realized by any model of the following enrichment of Set: SetDelete =def enrich Set by opns delete : elem bunch ! bunch axioms delete(a; B ) = removeone(a; B ) The de nition of delete as removeone takes advantage of the fact that in Set, each element occurs at most once in a bunch. Now, suppose we view the de nition BunchDelete =def Delete(Bunch) as a design speci cation which decomposes the task of implementing BunchDelete into two subtasks: 1. Implement Bunch. 2. Implement Delete] , where Delete] is given explicitly as follows: Delete] = A:Bunch: enrich fAg by opns delete : elem bunch ! bunch axioms count(a; delete(a; B )) = 0 a 6= b ) count(a; delete(b; B )) = count(a; B ) correct implementation of the design speci cation. The rst part is indeed a correct implementation of Bunch, but the second part is not a correct implementation of Delete] . It works only in the context of the particular implementation of Bunch we have chosen since it takes advantage of some of its properties which are not shared by other possible implementations. Thus it disobeys the principle of modular decomposition by which separate modules are to be implemented independently. The natural implementation of Delete] would de ne delete to repeatedly apply removeone until all occurrences of the given element are removed. Applying this implementation to any model of Set gives the same algebra as the extension embodied in SetDelete (this does not happen in all examples | see Example 4.22) but the \code" would be quite di erent. Most signi cantly, the modular version would be reusable in other contexts since its correctness is preserved under a change of the implementation of Bunch. of Bunch above by operations to choose an element of a non-empty bunch, to test whether a bunch d is empty, and to form the union of two bunches. Let Set be an analogous enrichment of Set, and let \ \ Delete be like Delete but with the range of admissible parameters determined by Bunch rather than by Bunch. Then Suppose we regard SetDelete as consisting of two separate parts: an implementation of Bunch (i.e. Set) together with an enrichment of this which adds delete de ned as removeone. This is not a \ Example 4.22 A variation on the above example is the following. Consider an enrichment Bunch \ \ Delete = A:Bunch: enrich fAg ] ] by opns delete : elem bunch ! bunch axioms : : : \ One possible implementation of Delete would code delete (a; B ) by rst initialising the result to empty, and then, while B is non-empty, choosing an element of B , removing it from B , and if the chosen element is di erent from a, adding it to the result. Such an implementation is quite natural under an 20 assumption that the count operation is relatively \expensive" and the other operations are relatively \cheap" | which is quite likely under (for example) the most obvious list implementation of bunches. d \] Applying this implementation of Delete to an implementation of Set yields, of course, an imple\d mentation of Delete (Set ). \d However, if we were to realize Delete (Set ) directly, even assuming that we use a similar idea for the implementation, then the most natural algorithm for delete (a; B ) would proceed as above only to the point where the rst (and only) occurrence of a in B is encountered. Then the search would stop, and the union of the result accumulated so far with the remainder of B would be the answer (since these two parts are disjoint, forming their union is cheap). The algebra thus obtained would \] be di erent from that obtained by instantiating the parametric implementation of Delete sketched above. 5 Higher-order parameterisation The ASL-style -calculus approach to parameterised speci cations, outlined in Section 3, extends naturally to a higher-order parameterisation mechanism. (A very limited form of this in the pushout approach to parameterisation is provided by parameterised parameter passing EM 85].) By allowing both the arguments and results of parameterised speci cations to be parameterised speci cations of an arbitrary complexity, as suggested in ST 88a], we obtain a hierarchy of higher-order parameterised speci cations. This hierarchy is indexed by a class of types T de ned as the least class such that: For any signature , 2 T ; and For any types 1; 2 2 T , 1! 2 2 T . De nition 5.1 The semantic domain ParSpec( ) of (denotations of) parameterised speci cations of type 2 T is de ned inductively as follows: If = , then ParSpec( ) =def Pow (Alg ( )) (ordered by inclusion); this will be written as Spec ( ) as well. If = 1! 2, then ParSpec( ) =def ParSpec( 1) ! ParSpec ( 2), the class of monotone functions from ParSpec ( 1) to ParSpec( 2) (ordered by pointwise extension of the ordering on ParSpec ( 2)). This covers rst-order parameterisation (see De nition 4.1) since ParSpec ( 1! 2) = Spec ( 1) ! 1 : : : ! : : : 2 : : :) is the same as (: : : Spec ( 1 ) : : : ! : : : Spec ( 2 ) : : :). Similar de nitions may be formulated for parameter speci cations in place of parameter signatures, which will be done in Section 7. For now we will use an obvious modi cation of the notation introduced in Section 3. Example 5.2 The requirements speci cation in Example 4.21 may be rephrased using higher-order parameterisation. The most natural way to view Bunch is as a parameterised speci cation, parameterised by the type of elements. As before, Bunch serves as a parameter for Delete, which then becomes a higher-order parameterised speci cation. Let Elem =def sorts elem Spec ( 2). In general, ParSpec (: : : 21 and P-Bunch =def ESP :Spec (Elem): add : elem bunch ! bunch removeone : elem bunch ! bunch count : elem bunch ! nat axioms count(a; empty) = 0 count(a; add(a; B )) > 0 = true a 6= b ) count(a; add(b; B )) = count(a; B ) count(a; B ) = 0 ) count(a; removeone(a; B )) = 0 count(a; B ) 6= 0 ) count(a; removeone(a; B )) = count(a; B ) ? 1 a 6= b ) count(b; removeone(a; B )) = count(b; B ) on fbunchg Let Bunch reachable enrich ESP + Nat by sorts bunch opns empty : ! bunch be the result signature of P-Bunch. Then P-Bunch : Spec (Elem ) ! Spec ( BSP :Spec (Elem) ! Spec ( Bunch): ESP :Spec (Elem): enrich BSP (ESP ) Bunch ). P-Delete =def by opns delete : elem bunch ! bunch axioms count(a; delete(a; B )) = 0 a 6= b ) count(a; delete(b; B )) = count(a; B ) We now have P-Delete : (Spec (Elem) ! Spec ( Bunch)) ! (Spec (Elem) ! Spec ( Delete)) where Delete is Bunch together with the new operation delete : elem bunch ! bunch . We can thus apply P-Delete to P-Bunch, and then P-Delete(P-Bunch) : Spec (Elem ) ! Spec ( Delete ) is a parameterised speci cation of bunches with the delete operation, parameterised by the type of elements. Finally, P-Delete(P-Bunch)(Elem ) : Spec ( Delete ) is a non-parameterised speci cation of bunches of arbitrary elements with the delete operation. This is the same as the requirements speci cation BunchDelete of Example 4.21. Our earlier discussion said that it is often possible to turn a requirements speci cation directly into a design speci cation, leading towards an implementation having the same structure as the requirements speci cation. Applying this design strategy to the above example naturally leads to the need for higher-order parameterisation of software modules. We will be talking about software modules (corresponding to P-Delete) parameterised by software modules (corresponding to P-Bunch) which are themselves parameterised (by a realization of Elem). To model this we need higher-order parametric algebras. The generalisation is not di cult: we introduce a hierarchy of higher-order parametric algebras indexed by the class T of types. De nition 5.3 The class Alg ( ) of parametric algebras of type 2 T is de ned inductively as follows: If = , then Alg ( ) is the class of all -algebras. 22 If = 1! 2, then Alg ( ) =def Alg ( 1) ! Alg ( 2), the class of all functions from Alg ( 1) to Alg ( 2). The semantic domain Spec ( ) of (denotations of) speci cations of parametric algebras of type 2 T is de ned as Pow (Alg ( )), ordered by inclusion. This covers rst-order parameterisation (see De nition 4.2), since Spec ( 1! 2) as de ned here is the same as Spec ( 1 ! 2) as de ned there. This will be generalised further in Section 7. For now we will use an obvious modi cation of the notation introduced in Section 3 for speci cations of parametric algebras. As before, there is a natural connection between the semantic domains of parameterised speci cations and speci cations of parametric algebras having the same type. The following de nition generalises De nition 4.5. De nition 5.4 For any type 2 T , we de ne by induction: For any P 2 ParSpec ( ), let P ] 2 Spec ( ) be de ned by: { If = , P ] =def P . { If = 1! 2, then P ] =def fF 2 Alg ( ) j for all A 2 Alg ( 1), F (A) 2 P (fAgy)]g. For any Q 2 Spec ( ), let Qy 2 ParSpec ( ) be de ned by: { If = , Qy =def Q. { If = 1! 2, then Qy(C ) =def FA2C] fF (A) j F 2 Qgy for any C 2 ParSpec ( 1), where t is the least upper bound in ParSpec ( 2) with respect to the ordering of De nition 5.1. Proposition 4.7 and Corollary 4.8 carry over to this more general framework as well (the monotonicity of parameterised speci cations is needed to show this). It is possible to further generalise this to the case where we have parameter speci cations rather than parameter types, but the details are rather involved. Armed with the above technicalities, let us go back to our example. Example 5.5 Suppose that BunchDelete =def P-Delete(P-Bunch)(Elem) is the requirements speci cation we are to implement. Viewing this de nition as a design speci cation, we decompose the task of implementing BunchDelete into three subtasks: 1. Implement Elem. 23 2. Implement P-Bunch] , where P-Bunch] is given explicitly as follows: P-Bunch] = A:Elem: enrich fAg + Nat by sorts bunch opns empty : ! bunch add : elem bunch ! bunch removeone : elem bunch ! bunch count : elem bunch ! nat axioms count(a; empty) = 0 count(a; add(a; B )) > 0 = true a 6= b ) count(a; add(b; B )) = count(a; B ) count(a; B ) = 0 ) count(a; removeone(a; B )) = 0 count(a; B ) 6= 0 ) count(a; removeone(a; B )) = count(a; B ) ? 1 a 6= b ) count(b; removeone(a; B )) = count(b; B ) 3. Implement P-Delete(]) , where P-Delete(]) is de ned as a restriction of P-Delete] to the domain of interest as follows: P-Delete(]) =def F :P-Bunch]: A:Elem: enrich fF (A)g by opns delete : elem bunch ! bunch axioms count(a; delete(a; B )) = 0 a 6= b ) count(a; delete(b; B )) = count(a; B ) Given any realization of these tasks, that is: 1. any algebra A 2 Elem ] ; 2. any parametric algebra F 2 P-Bunch]] ; and 3. any higher-order parametric algebra G 2 P-Delete(])] an implementation of the requirement speci cation BunchDelete may be constructed, namely G(F )(A) 2 BunchDelete ] . We stress once more that turning a requirements speci cation directly into a design speci cation is not the only way to proceed. It is important to allow the design speci cation to take on a completely di erent structure from the requirements speci cation if necessary. The above example illustrates that higher-order parameterisation is sometimes necessary to present speci cations and to structure implementations in a natural way. Another more extended example is given in the appendix of SST 90]; see also Sok 90]. 6 Program development Higher-order parameterisation is not only useful for purposes of presentation, as we saw in the previous section; it also comes in during the process of developing modular programs from speci cations. The view of program development presented in ST 88b], ST 92] and further elaborated for the Extended ML framework in ST 89] is based on the notion of a constructor implementation: 24 De nition 6.1 Let SP be a speci cation of (parametric) algebras of type 2 T and let SP1; : : :; SPn be speci cations. A constructor from hSP1; : : :; SPn i to is a function : S P1] ! : : : ! S Pn ] ! Alg ( ). We say that SP is implemented by hSP1; : : :; SPn i via , written SP > hSP1; : : :; SPni, if for all A1 2 S P1] ; : : :; An 2 S Pn ] , (A1) (An ) 2 S P ] . If SP > hSP1; : : :; SPn i, then given any realizations A1 2 S P1] ; : : :; An 2 S Pn ] , the constructor yields a realization of SP , namely (A1) (An) 2 S P ] . For technical convenience we have assumed here that constructors, which may naturally be viewed as multi-argument functions, are given in their curried form. The program development process builds a tree of constructor implementations having the original requirements speci cation as its root and speci cations of subtasks yet to be achieved as leaves. 8 > > SP1 > 1 > >. >. >. > < 8 > SPn1 > SP > > > < n1 > > SP > > n > n> > > > : : S Pnm > nm This process is nished once a tree is obtained which has speci cations with known implementations, given as parameterless constructors, as its leaves. 8 > SP1 > hi > 1 > > >. >. >. > < n 8 > SPn1 SP > > SPn11 n11 > hi > > < n1 > > SP > > n n> > > > > > : S Pnm : > hi nm Then the composition of the constructors in the tree yields a realization of the original requirements speci cation. The above tree yields ( 1) ( n ( n1( n11)) ( nm)) 2 S P ] : An obvious observation here is that constructors (in their curried form) are parametric algebras. This view was presented in ST 88b] but was limited there to speci cations of non-parametric algebras; in particular the type of algebras speci ed by SP was always a signature. In the current framework it is natural to consider the generalisation of this view to the case where any of the speci cations involved in the development process is a speci cation of (possibly higher-order) parametric algebras. For example, one might wish to use an implementation such as SP > hSP1; SP2i where SP : Spec ( ), SP1 : Spec ( 1) and SP2 : Spec ( 1 ! ). The constructor would be a function : S P1] ! S P2] ! Alg ( ) de ned by (A1)(F2) = F2(A1). A correct implementation is obtained provided that for any A1 2 S P1] and F2 2 S P2] , F2(A1) 2 S P ] . This holds, for instance, if we let SP2 =def A:SP1: SP , which decomposes the problem of implementing SP into the problem of implementing SP1 and (independently) implementing SP2. The latter is the problem of implementing SP given an (arbitrary) implementation of SP1. In general, higher-order parameterisation allows us to restrict to constructors which are of a particularly simple form. Namely, any constructor implementation SP > hSP1; : : :; SPn i may be replaced by the decomposition SP app > hSP ; SP1; : : :; SPni, where SP = X1:SP1: Xn :SPn: SP and app = F :SP : X1 :SP1: Xn :SPn : FX1 : : :Xn , and then the realization of SP by the constructor (which is correct since SP > hSP1; : : :; SPni means 2 S P ] ). Such a decomposition 25 captures the decision to realize SP in terms of realizations of SP1; : : :; SPn , turning the problem of nding the necessary construction into yet another subtask. If n = 0 then this is pointless since no progress is made towards a realization. Even if n > 0, from the methodological point of view one may question whether it is appropriate to postpone the problem of nding a constructor in this manner. This is exactly the controversy between advocates of the top-down development style (as captured by SP > hSP1; : : :; SPn i) and the bottom-up development style (as captured by SP app > hSP ; SP1; : : :; SPni). We believe that steps of both kinds are useful, and indeed in this formulation the distinction is somewhat blurred, with a spectrum of possibilities between these two extremes. Example 6.2 Example 5.5 may be rephrased as a higher-order constructor implementation step BunchDelete > hElem; P-Bunch]; P-Delete(])i where : Elem] ! P-Bunch]] ! P-Delete(])] ! Alg ( Delete ) is de ned by (A)(F )(G) =def G(F )(A) for arbitrary A 2 Elem] , F 2 P-Bunch]] and G 2 P-Delete(])] . If we restrict attention to the case in which all the speci cations involved are Extended ML functor speci cations (recall that these amount to speci cations of rst-order parametric algebras), the framework obtained corresponds to the Extended ML formal program development methodology described in ST 89], ST 91b] (modulo issues of behavioural equivalence). The main kind of development step in this framework is the decomposition of an Extended ML functor speci cation into a number of simpler Extended ML functor speci cations. The constructor involved in this step describes how to build a functor which realizes the original functor speci cation out of functors which realize the simpler functor speci cations. Example 6.3 A simple case is the decomposition of the speci cation FSP =def into the two speci cations via the constructor X :SPin : SPout X :SPin: SP 0 Y :SP 0: SPout GSP =def HSP =def G:GSP: ( H :HSP: ( X :SPin : H (G(X )))) This splits the task of implementing FSP into rst implementing SP 0 given any model of SPin , and separately implementing SPout given any model of SP 0. the model of SPin which is available to the implementor of GSP . This suggests that a possibly more exible decomposition of FSP might be into the speci cations Example 6.4 When the decomposition is as in Example 6.3, the implementor of HSP cannot use GSP =def HSP =def X :SPin : SP 0 0 X :SPin : ( Y :SP : SPout) could have done in the rst-order framework described in ST 89], ST 91b]. 26 G:GSP: ( H :HSP: ( X :SPin : H (X )(G(X )))) The uncurried version of this (where HSP is a two-argument functor speci cation) is the best we via the constructor Example 6.5 We can use higher-order parameterisation to go further than in Example 6.4 and make the realization of GSP available to the implementor of HSP . We decompose the task of implementing FSP into the speci cations GSP =def HSP =def via the constructor X :SPin : SP 0 X :SPin : ( G:GSP: SPout ) The implementor of HSP now has more powerful tools available to use in building a realization of SPout . Previously, only a realization X of SPin and a particular realization G(X ) of SP 0 were made available; now G itself is available as well, which means that G(X ) as well as applications of G to other algebras satisfying SPin can easily be obtained. Note that there is nothing methodologically ugly about this: there are two independent implementation tasks to perform, one of implementing GSP and the other of implementing HSP , and a strict separation between the two tasks is preserved. The implementor of HSP is provided with a realization of GSP , but he can rely only on those features of this realization which are explicitly stated in GSP . The use of higher-order parameterisation as in the above example is not merely a specious generalisation. Consider the problem of implementing an interpreter for a programming language. An obvious subtask of this is to implement stacks, since stacks are useful in various places including the parser (stacks of parse trees) and the evaluator (stacks of data values). Using rst-order parameterisation as in Example 6.4, we would decompose the task of implementing the interpreter into the following subtasks: 1. Implement stacks of arbitrary elements. 2. Implement parse trees. 3. Implement data values. 4. Implement the interpreter, using parse trees, data values, stacks of parse trees and stacks of data values. However, the implementor of subtask 4 may notice that yet another kind of stacks are required, perhaps in the symbol table. In a strict rst-order regime, he/she would either have to re-implement stacks for this purpose, or else go back to the designer and ask for the speci cation of his/her subtask to be modi ed to provide the new instantiation of stacks. But using higher-order parameterisation as in Example 6.5, subtask 4 would become 4. Implement the interpreter, using parse trees, data values and stacks of arbitrary elements. Stacks of parse trees and of data values would be constructed during the realization of this subtask, as would stacks of other kinds of elements if the need arises. An alternative decomposition would be into just two subtasks: 1. Implement stacks of arbitrary elements. 2. Implement the interpreter, using stacks of arbitrary elements. 27 G:GSP: ( H :HSP: ( X :SPin : H (X )(G))) This leaves the implementation of parse trees and data values as potential lower-level subtasks of subtask 2. Such a decomposition introduces a bottom-up avour into our top-down design methodology, as mentioned above. It may turn out that the implementor of subtask 2 does not need stacks at all; they are provided as tools which might come in handy for the task at hand. In some such cases, explicit higher-order parameterisation may be avoided. An environment of previously-de ned modules, all of which are available for use in subsequent module de nitions, allows some higher-order dependencies of the kind illustrated above to be left implicit. However, this trick does not work when dependencies become complex and deeply nested, and anyway it seems advisable to keep dependencies explicit rather than trying to sweep them under the carpet. In the preceding sections we have argued for the use of both parameterised speci cations and speci cations of parametric algebras (and of their higher-order counterparts) in software speci cation and development. In this section, we present a speci cation formalism which extends in an essential way the kernel speci cation language presented in ST 88a] by adding a simple yet powerful parameterisation mechanism which allows us to de ne and specify parametric algebras of arbitrary order, as well as extending the mechanism in ST 88a] for de ning rst-order parameterised speci cations to the higher-order case. This is achieved by viewing speci cations on one hand as speci cations of objects such as algebras or parametric algebras, and on the other hand as objects themselves to which functions (i.e. parameterised speci cations) may be applied. Consequently, the language allows speci cations to be speci ed by other speci cations, much as in CLEAR BG 80] or ACT ONE EM 85] parameterisation where the parameter speci cation speci es the permissible argument speci cations (see Section 3). The view of speci cations as objects enables the use of a uniform parameterisation mechanism, functions de ned by means of -abstraction, to express both parameterised speci cations and parametric algebras. There is also a uniform speci cation mechanism to specify such functions, -abstraction (Cartesian-product speci cation, closely related to the dependent function type constructor in e.g. NuPRL Con 86]). This may be used to specify (higher-order) parametric algebras as well as (higherorder) parameterised speci cations. There is no strict separation between levels, which means that it is possible to intermix parameterisation of objects and parameterisation of speci cations, obtaining (for example) algebras which are parametric on parameterised speci cations or speci cations which are parameterised by parametric algebras. We have not yet explored the practical implications of this technically natural generalisation. The language does not include notation for describing algebras, signatures, signature morphisms, or sets of sentences. Such notation must be provided separately, for example as done for ASL in Wir 86]. The de nition of the language is independent of this notation; moreover, it is essentially institution independent, with all the advantages indicated in GB 84], ST 88a]. 7.1 Introducing the language 7 A kernel speci cation formalism 28 The language has just one syntactic category of interest, which includes both speci cations and objects that are speci ed, with syntax as follows: Object = j j j j j j j j j j j j j j Signature impose Sentences on Object derive from Object by Signature-morphism translate Object by Signature-morphism minimal Object wrt Signature-morphism iso-close Object abstract Object wrt Sentences via Signature-morphism Object Object Variable:Object: Object fObjectg Spec(Object) Variable Algebra-expression Variable:Object: Object Object (Object) 9 > > > > > > > > > > > = > > > > > > > > > > > ; 9 > > > = > > > ; 9 > > > = > > > ; Simple speci cations Other speci cations Other objects As usual, we have omitted the \syntax" of variables. The other syntactic categories of the language above are algebra expressions, signatures, sets of sentences and signature morphisms | as mentioned above, the details of these are not essential to the main ideas of this paper and we assume that they are provided externally. Algebra expressions may contain occurrences of object variables. We will assume, however, that variables do not occur in signatures, signature morphisms and sentences, which seems necessary to keep the formalism institution-independent. This requirement may seem overly restrictive, as it seems to disallow the components of a particular algebra to be used in axioms; one would expect to be able to write something like X : : (: : :X:op : : :). Fortunately, using the power of the speci cation-building operations included in the language, it is possible to de ne a more convenient notation which circumvents this restriction (see the appendix of SST 90]). We have used the standard notation for - and -objects to suggest the usual notions of a free and of a bound occurrence of a variable in a term of the language, as well as of a closed term. As usual, we identify terms which di er only in their choice of bound variable names. We de ne substitution of objects for variables in the usual way: Obj Obj 0=X ] stands for the result of substituting Obj 0 for all free occurrences of X in Obj in such a way that no unintended clashes of variable names take place. This also de nes the usual notion of -reduction between objects of the language: (: : : ( X :SP: Obj )(Obj 0) : : :) ! (: : :Obj Obj 0=X ] : : :). Then, ! is the re exive and transitive closure of ! . The rst seven kinds of speci cations listed above (simple speci cations) are taken directly from ST 88a] (see Section 2). The particular choice of these seven operations is orthogonal to the rest of the language and will not interfere with the further development in this paper. We have singled out the union operation | we will use it for arbitrary, not necessarily \simple" speci cations (this generalisation w.r.t. ST 91a] makes the formalism more exible, but otherwise does not seem to cause any extra technical di culties). The other three kinds of speci cations are new. -abstraction is used to specify parametric objects.3 To make this work, it must be possible to use objects in speci cations. The f g operation provides this possibility by allowing objects to be turned into (very tight) speci cations. The next clause allows a speci cation which de nes a class C of objects to be turned into a speci cation which de nes the class of speci cations de ning subclasses of C . This is compatible with the use of parameter speci cations in parameterised speci cations as in 3 The notation SP ! SP 0 is often used for X :SP: SP 0 if X does not actually occur in SP 0 . 29 CLEAR and ACT ONE. For example, the declaration proc P (X : SP ) = : : : in CLEAR introduces a parameterised speci cation P , where the parameter (or requirement ) speci cation SP describes the admissible arguments of P . Namely, if SP de nes a class of objects C = S P ] then P may be applied to argument speci cations SParg de ning a subclass of C , i.e. such that S Parg ] S P ] (we disregard the parameter tting mechanism). In our formalism this would be written as P =def X :Spec(SP ): : : : . The syntax of other objects is self-explanatory. The richness of the language may lead to some di culty in recognizing familiar concepts which appear here in a generalised form. The following comments might help to clarify matters: A speci cation is (an object which denotes) a class of objects. If the objects of this class are algebras, then this speci cation is a speci cation in the usual sense. X :(: : :) : (: : :) denotes a class of mappings from objects to objects. If these objects are algebras, then this is a class of parametric algebras, i.e. a speci cation of a parameterised program. X :(: : :) : (: : :) denotes a mapping from objects to objects. If these objects are speci cations in the usual sense, then this is a parameterised speci cation. The semantics of the language, presented in the next section, gives more substance to the informal comments above concerning the intended denotations of certain phrases. As pointed out above, we assume that the sublanguage of expressions de ning algebras is to be supplied externally (with a corresponding semantics | see Section 7.2). Even under this assumption, it would be possible to include institution-independent mechanisms for building algebras from other algebras (amalgamation, reduct, free extension, etc.) in the language, which could lead to a powerful and uniform calculus of speci ed modular programs. This is an interesting possibility for future work but it is outside the scope of this paper. We have chosen the syntax for objects in the language so that their semantics should be intuitively clear. We formalise it by de ning for any environment , which assigns meanings to variables, a partial function ] mapping an object Obj to its meaning Obj ] . It is de ned below by structural induction on the syntax of objects. The use of the meta-variable SP instead of Obj in some places below is intended to be suggestive (of objects denoting object classes, used as speci cations) but has no formal meaning. This convention will be used throughout the rest of the paper. Simple speci cations: 7.2 Semantics impose on SP ] = fA 2 S P ] j A j= g if S P ] Alg ( ) and ] = Alg ( ) derive from SP by ] = fA j A 2 S P ] g Sen ( ) for some signature 0 if S P ] Alg ( ) and : 0 ! is a signature morphism for some signatures and : : : similarly for the other forms, based on the semantics given in Section 2 : : : 30 Other speci cations: S P S P 0] = S P ] \ S P 00] if S P ] and S P ] are classes of values fObj g] = f Obj ] g if Obj ] is de ned X :SP: SP 0] = v2 SP ] S P 0] v=X ]4,5 if S P ] is a class of values and for each v 2 S P ] , S P 0] v=X ] is a class of values Spec(SP )]] = Pow ( SP ] ) if S P ] is a class of values Other objects: de nitional clause holds. It is easy to see that the semantics of an object of the language depends only on the part of the environment which assigns meanings to variables which occur free in the object. In particular, the meaning of a closed object is independent from the environment. This allows us to omit the environment when dealing with the semantics of closed objects and write simply Obj ] to stand for Obj ] for any environment whenever Obj is closed. Of course, the above remark is true only provided that the sublanguage of algebra expressions and its semantics assumed to be given externally have this property. In the following, we will take this for granted. We will also assume that the sublanguage satis es the following substitutivity property: for any algebra expression A, variable X and object Obj , for any environment such that v = Obj ] is de ned, A Obj=X ]]] is de ned if and only if A] v=X ] is de ned, and if they are de ned then they are the same. This ensures that the following expected fact holds for our language (the standard proof by induction on the structure of objects is omitted): Fact 7.1 For any0 objects Obj , Obj 0 and variable X , for any environment such that v0 = Obj 0] is de ned, Obj Obj =X ]]] is de ned if and only if Obj ] v0=X ] is de ned, and if they are de ned then X ] = (X ) A] = : : : assumed to be given externally : : : X :SP: Obj ] = fhv 7! Obj ] v=X ]5i j v 2 S P ] g if S P ] is a class of values and for each v 2 S P ] , Obj ] v=X ] is de ned Obj (Obj 0 )]] = Obj ] ( Obj 0] ) if Obj ] is a function and Obj 0] is a value in the domain of this function In the above de nition, it is understood that a condition like \ SP ] Alg ( )" implicitly requires that S P ] is de ned. An object's meaning is unde ned unless the side-condition of the appropriate Obj Obj 0=X ]]] = Obj ] v0=X ] such that Obj ! Obj , for any environment , if Obj ] is de ned then so is Obj ] and Obj ] = Obj 0] . is, on the right-hand side of this de nition denotes the usual Cartesian product of an indexed family of sets. That is the set of all functions with domain S mapping any x 2 S to an element of Cx . 5 As usual, v=X ] is the environment which results from by assigning v to the variable X (and leaving the values of other variables unchanged). 4 Corollary 7.2 -reduction preserves the meaning of objects. That is, for any objects Obj and Obj 0 0 0 x2S Cx 31 The reader might feel uneasy about the fact that we have not actually de ned here any domain of values, the elements of which are assigned to objects of the language as their meanings. A naive attempt might have been as follows: V alues = Algebras j Pow (V alues) j V alues ! V alues e Clearly, this leads to serious foundational problems, as the recursive domain de nition involves \heavy recursion" (cf. BT 83]) and hence cannot have a set-theoretic solution (even assuming that we consider here a set Algebras of algebras built within a xed universe). However, since the formalism we introduce is not intended to cater for any form of self application of functions or non-well-foundedness of sets, the equation above attempts to de ne a domain of values of objects which is undesirably rich. The well-formed6 objects of the language can easily be seen to form a hierarchy indexed by \types" (see Section 7.4). Thus, we can de ne a corresponding cumulative hierarchy of sets of values, and then de ne the domain of the meanings of objects as the union of sets in the hierarchy, much in the style of BKS 88] (see BT 83] where the idea of using hierarchies of domains in denotational semantics is discussed in more detail). Another, less \constructive", possibility is to work within a xed universal set of values of objects containing the \set" of all algebras Coh 81]. We are interested in determining whether or not given objects satisfy given speci cations. We use the formal judgement Obj : SP to express the assertion that a closed object Obj satis es a closed speci cation SP , i.e. that Obj ] 2 S P ] , and generalise it to X1 : SP1; : : :; Xn : SPn ` Obj : SP stating the assertion that an object Obj satis es a speci cation SP in the context X1 : SP1; : : :; Xn : SPn , i.e. under the assumption that objects X1; : : :; Xn satisfy speci cations SP1; : : :; SPn, respectively. The inference rules listed below allow us to derive judgements of this general form. For the sake of clarity, though, we have decided to make contexts implicit in the rules and rely on the natural deduction mechanism of introducing and discharging assumptions (all of the form X : SP here) to describe the appropriate context manipulation. For example, in (R2) below, X : SP ] is an assumption which may be used to derive SP 0 : Spec(SP 00), but is discharged when we apply the rule to derive its conclusion. Whenever necessary, we will use the phrase \the current context" to refer to the sequence of currently undischarged assumptions. We say that an environment is consistent with a context X1 : SP1; : : :; Xn : SPn if for i = 1; : : :; n, (Xi ) 2 S Pi ] . Simple speci cations: 7.3 Proving satisfaction signature : Spec( ) SP : Spec( ) impose on SP : Spec( ) Sen ( ) SP : Spec( ) :!0 SP : Spec( 0) :!0 derive from SP by : Spec( ) translate SP by : Spec( 0) SP : Spec( ) : 0! minimal SP wrt : Spec( ) SP : Spec( ) 6 SP : Spec( ) iso-close SP : Spec( ) Sen ( 0) 0 :! abstract SP wrt 0 via : Spec( ) 0 An intuitive understanding of the notion of well-formedness involved is su cient here (we hope) | we introduce it formally in Section 7.3. 32 Other speci cations: Obj : SP fObj g : Spec(SP ) X : SP ] SP : Spec(SPany ) SP 0 : Spec(SP 00) X :SP: SP 0 : Spec( X :SP: SP 00) SP : Spec(SP 0) Spec(SP ) : Spec(Spec(SP 0)) Union: (R1) (R2) (R3) SP1 SP1 : Spec(SP ) SP2 : Spec(SP ) SP1 S P2 : Spec(SP ) S P2 : Spec(SPany ) Obj : SP1 Obj : SP2 Obj : SP1 S P2 -expressions: (R4) (R5) X : SP ] SP : Spec(SPany ) Obj : SP 0 X :SP: Obj : X :SP: SP 0 Obj : X :SP: SP 0 Obj 0 : SP Obj (Obj 0 ) : SP 0 Obj 0=X ] Obj : SP SP ! S P 0 Obj : SP 0 Obj : SP SP 0 : Spec(SPany ) SP 0 ! S P Obj : SP 0 Trivial inference: (R6) (R7) (R8) (R9) Obj : SPany Obj : fObj g (R10) 33 \Cut" Obj : SP SP : Spec(SP 0) Obj : SP 0 (R11) Semantic inference: SP : Spec( ) SP; SP 0 : Spec( ) A] 2 S P ] for all consistent with the current context (R12) A : SP SP ] S P 0] for all consistent with the current context (R13) SP : Spec(SP 0) Some of these rules involve judgements ( signature, Sen ( ), : ! 0 ) which are external to the above formal system. This is a natural consequence of the fact that the language does not include any syntax for signatures, sentences, etc. More signi cantly, there are two rules which involve model-theoretic judgements, referring to the semantics of objects given above. Following the usual practice, in the sequel we will simply write \Obj : SP " meaning \Obj : SP is derivable". The rules labelled Simple speci cations characterise the well-formedness of -speci cations built using the underlying speci cation-building operations included in the language. They directly incorporate the \syntactic" requirements of Section 2 on the use of these operations. Rules (R1), (R2) and (R3) play a similar role for the other speci cation-forming operations: singleton speci cation, Cartesian-product speci cation and Spec( ), respectively. Notice, however, that their speci cations are given here in a form which is as tight as possible. For example, for any SP : Spec( ) and Obj : SP , rule (R1) allows us to deduce fObj g : Spec(SP ) rather than just fObj g : Spec( ). The rst of the two rules related to the union operation, (R4), embodies the characterisation of well-formed union speci cations. The other, (R5), gives the obvious way to prove that an object satis es a (well-formed) union speci cation. The two rules are not quite satisfactory, as they do not seem to su ciently capture the interplay between union and the other operations | more work is needed here. The rules related to -expressions and their applications to arguments are quite straightforward. Rules (R6) and (R7) are the usual rules for -expression introduction and application, respectively. The assumption SP : Spec(SPany ) in rule (R6) asserts the well-formedness of the speci cation SP (see also (R2), (R9), (R10)). Whenever the meta-variable SPany is used below, it will play the same role as part of a well-formedness constraint. Notice that in order to prove X :SP: Obj : X :SP: SP 0, we have to prove Obj : SP 0 \schematically" for an arbitrary unknown X : SP , rather than for all values in the class S P ] (for the appropriate environments ). Rules (R8) and (R9) embody a part of the observation that -reduction preserves the semantics of objects (Corollary 7.2). Rule (R8) allows for -reduction and rule (R9) for well-formed -expansion of speci cations. A particular instance of the latter is Obj 0 : SP 0 Obj=X ] ( X :SP: SP 0)(Obj ) : Spec(SPany ) Obj 0 : ( X :SP: SP 0)(Obj ) 34 That is, in order to prove that an object satis es a speci cation formed by applying a parameterised speci cation to an argument, it is su cient to prove that the object satis es the corresponding reduct. However, we have not incorporated full -equality into our system; rules (R8) and (R9) introduce it only for speci cations. In particular, we have not included the following rule, which would allow well-formed -expansion of objects: Obj : SP An instance of this would be: Obj 0 : SPany Obj 0 : SP Obj 0 ! Obj Obj1 Obj2=X ] : SP ( X :SP2: Obj1)(Obj2 ) : SPany ( X :SP2: Obj1 )(Obj2) : SP Hence, in order to prove that a structured object ( X :SP2: Obj1)(Obj2) satis es a speci cation SP , it would su ce to show that the object is well-formed and to prove that its -reduct Obj1 Obj2=X ] satis es the speci cation. We think that this is not methodologically desirable: a proof of correctness of a program should follow the structure of the program, without any possibility of attening it out. So, to prove ( X :SP2: Obj1)(Obj2) : SP we have to nd an appropriate speci cation for the parameterised program X :SP2: Obj1, say X :SP2: Obj1 : X :SP2: SP1 such that SP1 Obj2=X ] = SP (actually, SP1 Obj2=X ] : Spec(SP ) is su cient). The other part of -equality for objects, -reduction, although not derivable in the system, is admissible in it7 (see ST 91a] for a proof sketch): Lemma 7.3 The following rule is an admissible rule of the system Obj : SP Obj ! Obj 0 Obj 0 : SP It might be interesting to enrich the system by the -reduction rule for objects given in the above lemma, or even more generally by some \operational semantics rules" for (the computable part of) the object language. This, however, would be quite orthogonal to the issues of object speci cation considered in this paper. Therefore, to keep the system as small and as simple as possible, the rule is not included in the system. Rules (R10) and (R11) embody trivial deductions which should be intuitively straightforward. Notice that SP : Spec(SP 0), as in the premise of (R11), asserts that speci cation SP imposes at least the same requirements as SP 0. Rules (R12) and (R13) refer directly to the semantics of objects. They embody the semantic veri cation process which is a necessary component of inference in the above formal system. These rules are deliberately restricted to the non-parametric case, since this is the point at which an external formal system is required; parameterisation is handled by the other rules. We do not attempt here to provide a formal system for proving the semantic judgements A] 2 S P ] and S P ] S P 0] for all environments consistent with the current context. This is an interesting and important research topic, which is however separate from the main concerns of this paper; some considerations and results A rule is admissible in a deduction system if its conclusion is derivable in the system provided that all its premises are derivable. This holds in particular if the rule is derivable in the system, that is, if it can be obtained by composition of the rules in the system. 7 35 on this may be found in e.g. ST 88a] and Far 92]. It is not possible to give a set of purely \syntactic" inference rules which is sound and complete with respect to the semantics above because of the power of the speci cation mechanisms included in the language (this is already the case for the subset of the language excluding parameterisation, presented in Section 2). As mentioned earlier, to make the rules as clear and readable as possible, the presentation of the system omits a full formal treatment of contexts. In particular, we should add two rules to derive judgements that a context is well-formed (here, hi is the empty context): hi is a well-formed context ?] ? is a well-formed context X is not in ? SP : Spec(SPany ) ?; X : SP is a well-formed context and then axioms X1 : SP1; : : :; Xn : SPn ` Xk : SPk , for k = 1; : : :; n, where X1 : SP1; : : :; Xn : SPn is a well-formed context. It is important to realise that contexts are sequences, rather than sets, and so we allow the variables X1; : : :; Xk to occur in SPk+1. We will continue omitting contexts throughout the rest of the paper. All the de nitions and facts given below (as well as above) are correctly stated for closed objects only, but are meant to be naturally extended to objects in a well-formed context. This will be done explicitly only within proofs where it is absolutely necessary. Similarly, we will omit in the following the environment argument to the semantic function for objects; all the environments thus implicitly considered are assumed to be consistent with the corresponding context. We hope that this slight informality will contribute to the readability of the paper without obscuring the details too much. The following theorem expresses the soundness of the formal system above with respect to the semantics given earlier. Theorem 7.4 For any object Obj and speci cation SP , if Obj : SP is derivable then Obj ] 2 S P ] (that is, S P ] is de ned and is a class of values and Obj ] is de ned and is a value in this class). Proof (sketch) By induction on the length of the derivation and by inspection of the rules. A complete formal proof requires, of course, a careful treatment of free variables and their interpretation (cf. the remark preceding the theorem). Thus, for example, rule (R6) really stands for: ? ` SP : Spec(SPany ) ?; X : SP ` Obj : SP 0 ? ` X :SP: Obj : X :SP: SP 0 X is not in ? where ? is a context. In the corresponding case of the inductive step we can assume that 1. S P ] 2 Spec(SPany )]] for all environments consistent with context ?, and 2. Obj ] 2 S P 0] for all environments consistent with context ?; X : SP and then we have to prove that X :SP: Obj ] 2 X :SP: SP 0] for all environments consistent with context ?. That is, taking into account the semantics of - and -expressions as given in Section 7.2, we have to prove that for all environments consistent with context ? S P ] is de ned and is a class of values | which follows directly from assumption (1) above, and then for all values v 2 S P ] , 36 { Obj ] v=X ] is de ned, { S P 0] v=X ] is de ned and is a class of values, and { Obj ] v=X ] 2 S P 0] v=X ], which in turn follow directly from assumption (2) above. The cases corresponding to the other rules of the system require similar, straightforward but tedious analysis. Notice that the proofs about the rules concerning application and -reduction, (R7), (R8) and (R9), crucially depend on Fact 7.1 and Corollary 7.2. It is natural to ask if the above formal system is also complete with respect to the semantics. It turns out not to be complete. One reason for incompleteness is that the formal system does not exploit the semantical consequences of inconsistency. For example, for any inconsistent speci cation SP we have that S P ] 2 Spec(SPany )]] for any SPany such that S Pany ] is a class of values. The corresponding formal judgement SP : Spec(SPany ) is not derivable when (for example) SP and SPany are simple speci cations over di erent signatures. If the formal parameter speci cation in a - or expression is inconsistent then similar di culties arise (cf. MMMS 87] for a discussion of the related issue of \empty types" in typed -calculi). This topic deserves further study; it would be nice to identify all sources of incompleteness and the e ect of the deliberate omission of a rule allowing for well-formed -expansion of objects. De nition 7.5 An object Obj is well-formed if Obj : SP for some SP . This also de nes the well-formed speci cations since speci cations are objects. Checking whether an expression in the language is well-formed must in general involve \semantic" veri cation as embodied in rules (R12) and (R13). In fact, checking the well-formedness of objects is as hard as checking if they satisfy speci cations: Obj : SP if and only if ( X :SP: (any constant))(Obj ) is well-formed. An easy corollary to the soundness theorem is the following: Corollary 7.6 Any well-formed object Obj has a well-de ned meaning Obj ] . Since speci cations do not form a separate syntactic category of the language, in the above discussion we have used the term \speci cation" and the meta-variable SP rather informally, relying on an intuitive understanding of the role of the objects of the language. This intuitive understanding may be made formal as follows: De nition 7.7 An object SP is called a speci cation if for some SPany , SP : Spec(SPany ). Corollary 7.8 The meaning of a speci cation is a class of values: if SP : Spec(SPany ) then S P ] S Pany ] . Note that this covers ordinary -speci cations, speci cations of (higher-order) parametric algebras, speci cations of (higher-order) parameterised speci cations, etc. The following theorem shows that this is indeed consistent with our previous informal use of the term. Theorem 7.9 If Obj : SP then SP is a speci cation. Even though this theorem captures an intuitively rather obvious fact, its inductive proof (given in ST 91a], omitted here) is surprisingly long and relatively complicated. Unfortunately, this seems to be typical of many proofs dealing with \syntactic" properties of -calculi. 37 Inference in the system presented in the previous section has a purely \type-checking" component on which the \veri cation" component is in a sense superimposed. We try to separate this \typechecking" process below. The concept of type we use must cover signatures (as \basic types" of algebras) and \arrow types" (types of functions) which would be usual in any type theory, as well as \speci cation types" which are particular to the formalism presented here: as we have stressed before, the type of a speci cation is distinct from the type of objects the speci cation speci es. De nition 7.10 The class of types T is de ned as the least class such that: for any signature , 2 T ; for any types 1; 2 2 T , 1! 2 2 T ; and for any type 2 T , Spec( ) 2 T . Under the standard notational convention that arrow types of the form ! 0 stand for -types of the form X : : 0 where X does not actually occur in 0, types as de ned above are well-formed speci cations. We de ne type Type (Obj ) for an object Obj of our system by induction as follows: Simple speci cations: Type ( ) = Spec( ) 7.4 Type-checking signature Type (SP ) = Spec( ) Sen ( ) Type (impose on SP ) = Spec( ) Other speci cations: : : : and similarly for other simple speci cations : : : Type (fObj g) = Spec( ) Type (Spec(SP )) = Spec(Spec( )) Type (X ) = ] Type (SP ) = Spec( ) Type (SP 0) = Spec( 0) Type ( X :SP: SP 0 ) = Spec( ! 0) Union: Type (SP1) = Spec( ) Type (SP2) = Spec( ) Type (SP1 S P2) = Spec( ) -expressions: Type (X ) = ] Type (SP ) = Spec( ) Type (Obj ) = 0 Type (Obj ) = ! 0 Type (Obj 0 ) = Type ( X :SP: Obj ) = ! 0 Type (Obj (Obj 0 )) = 0 Algebra expressions: Type (Obj ) = Type (SP ) = Spec( ) A is an algebra expression denoting a -algebra Type (A) = 38 Note that the semantic inference rules (R12), (R13), the trivial inference rule (R10), the \cut" rule (R11), (R5) and the -reduction and -expansion rules (R8) and (R9), which do not introduce new well-formed objects, do not have counterparts in the above de nition. Clearly, the above de nition depends on a judgement whether or not an algebra expression denotes an algebra over a given signature. We will assume that such \type-checking" of algebra expressions is de ned externally in such a way that it is consistent with the semantics (i.e., if A is a well-formed algebra expression denoting a -algebra then indeed A] 2 Alg ( )). Moreover, we will assume that it is substitutive: if A is an algebra expression denoting a -algebra under an assumption Type (X ) = then for any object Obj with Type (Obj ) = , A Obj=X ] is an algebra expression denoting a -algebra as well. The above rules (deliberately) do not de ne Type(Obj ) for all object expressions of our language. However, if a type is de ned for an object, it is de ned unambiguously. An object Obj is roughly well-formed if its type Type(Obj ) is de ned. There are, of course, roughly well-formed objects that are not well-formed. The opposite implication holds, though: Theorem 7.11 Type (Obj ) is well-de ned for any well-formed object Obj . In particular: 1. If Obj : SP then Type (SP ) = Spec(Type (Obj )). 2. If SP is a speci cation then Type (SP ) = Spec( ) for some type . 3. If Obj : X :SP: SP 0 then Type (Obj ) = ! 0, where Type (SP ) = Spec( ), for some types and 0. We omit the proof here: the rst part of the theorem follows by induction on the length of the derivation of Obj : SP (this proof is sketched in ST 91a]). The other two parts follow directly from this. The above theorem states that a necessary condition for an object to satisfy a speci cation is that both are roughly well-formed and the type of the object is consistent with the type of the speci cation. Of course, nothing like the opposite implication holds. As pointed out earlier, proving that an object satis es a speci cation must involve a veri cation process as embodied in the two rules of semantic inference. One might now expect that any well-formed object Obj \is of its type", i.e. Obj : Type (Obj ). This is not the case, though. The problem is that both - and -expressions include parameter speci cations rather than just parameter types, and so functions denoted by -expressions and speci ed by -expressions have domains de ned by speci cations, not just by types. This is necessary for methodological reasons: we have to be able to specify permissible arguments in a more re ned way than just by giving their types. However, as a consequence, objects denoted by - and -expressions in general do not belong to the domain de ned by their types, and so we cannot expect that such expressions would \typecheck" to their types. To identify the purely \type-checking" component in our system we have to deal with objects where parameter speci cations are replaced by their types. Formally, for any roughly well-formed object Obj , its version Erase (Obj ) with parameter speci cations erased is de ned by \rounding up" parameter speci cations to parameter types. A full inductive de nition is given in ST 91a]; two crucial cases are: Erase ( X :SP: SP 0 ) =def X : : Erase (SP 0) where Type (Erase (SP )) = Spec( ) Erase ( X :SP: Obj ) =def X : : Erase (Obj ) where Type (Erase (SP )) = Spec( ) 39 the version of the object where parameter speci cations have been \rounded up" to parameter types, has a type which is consistent with the type of the speci cation. This necessary condition embodies the purely type-checking component of any proof that an object satis es a speci cation. It is important to realize that the type-checking of Erase (Obj ) may be performed within the original system, since Type (Erase (Obj )) = if and only if Erase (Obj ) : Spec( ). Moreover, this can be done separately from the semantic veri cation part, without any reference to the meanings of objects and speci cations. We present below the corresponding proper fragment of the original system: Simple speci cations: Sen ( ) signature SP : Spec( ) : Spec( ) impose on SP : Spec( ) Obj , Erase (Obj ) is well-formed and has the same type as Obj . Joining this with Theorem 7.11, we conclude that a necessary condition for an object Obj to satisfy a speci cation is that Erase (Obj ), Now, by a tedious but straightforward induction one may show that for any roughly well-formed object : : : and just as before for other simple speci cations : : : Other speci cations: Obj : fObj g : Spec( ) X: ] SP 0 : Spec( 0) SP : Spec( ) 0 0 X : : SP : Spec( ! ) Spec(SP ) : Spec(Spec( )) Union: SP1 : Spec( ) SP2 : Spec( ) SP1 S P2 : Spec( ) -expressions: X: ] Obj : 0 X : : Obj : ! 0 Obj : ! 0 Obj 0 : Obj (Obj 0) : 0 Algebra expressions: A is an algebra expression denoting a -algebra A: We hope that a comparison of the above with the system presented in Section 7.3 will clearly illustrate the intuitive di erence between typed -calculi, like the one above, and \speci ed" -calculi, like the one in Section 7.3. Example 7.12 Let us look again at Example 5.2. 7.5 An example First, since Elem is just a signature, Type (Elem ) = Spec(Elem ). Moreover, we have Elem : Spec(Elem) 40 Then, P-Bunch as de ned before is well-formed (modulo the necessary translation of +, enrich and reachable into the operations provided by the system) and has type Spec(Elem )!Spec( Bunch ). Again, because Elem is a trivial speci cation, we have P-Bunch : Spec(Elem)!Spec( Bunch) It is possible, however, to derive a much tighter speci cation of P-Bunch than its type: P-Bunch : E :Spec(Elem): Spec(P-Bunch(E )) Then another, perhaps more adequate, version of P-Delete may be de ned as follows: P-Delete0 =def BSP :( E :Spec(Elem): Spec(P-Bunch(E ))): ESP :Spec(Elem): enrich BSP (ESP ) by opns delete : elem bunch ! bunch axioms count(a; delete(a; B )) = 0 a 6= b ) count(a; delete(b; B )) = count(a; B ) Bunch)) ! (Spec(Elem) ! Spec( Delete)) Then Type (P-Delete0 ) = (Spec(Elem) ! Spec( much as in Example 5.2. However, we do not have P-Delete0 : (Spec(Elem) ! Spec( Bunch)) ! (Spec(Elem) ! Spec( Delete)) The type of P-Delete 0, viewed as a speci cation, requires the speci ed objects (which are higherorder parameterised speci cations) to be applicable to any speci cation of the type Spec(Elem ) ! Spec( Bunch ), which is not the case with P-Delete 0 as de ned here. We can, however, show that P-Delete0 : ( E :Spec(Elem): Spec(P-Bunch(E ))) ! (Spec(Elem) ! Spec( and the tightest speci cation we can derive for P-Delete 0 is P-Delete0 : B : E :Spec(Elem): Spec(P-Bunch(E )) : Delete)) E :Spec(Elem): Spec(P-Delete0(B )(E )) 8 Concluding remarks In this paper we have discussed parameterisation and its role in the process of software speci cation and development. We have especially stressed two points. The rst is that there should be a clear distinction between parameterised speci cations and speci cations of parameterised software: parameterised (program speci cation) 6= (parameterised program) speci cation Both concepts are important and useful, but they are modelled by di erent semantical objects and, more signi cantly, they play di erent roles in the process of software development. The methodological consequences of this distinction were discussed in detail in Section 4.3. 41 The second point is that it is natural and useful to generalise parameterisation to the higherorder case. Speci cations of higher-order parametric program modules arise naturally and give extra exibility in the process of systematic software development. This was discussed in Sections 5 and 6. Spurred by these methodological considerations, in Section 7 we introduced an institution-independent speci cation formalism that provides a notation for parameterised speci cations and speci cations of parametric objects of an arbitrary order, as well as any mixture of these concepts. The formalism incorporates the kernel speci cation-building operations described in ST 88a] based on those in the ASL speci cation language SW 83], Wir 86]. The basic idea was to treat speci cations, which specify objects, as objects themselves. This collapsing together of the two levels, that of objects and that of their speci cations, led (perhaps surprisingly) to a well-behaved inference system for proving that an object satis es a speci cation with a clearly identi ed formal type-checking component. The formalism presented deals explicitly with two levels of objects involved in the process of software development: programs (viewed as algebras) and their speci cations (viewed as classes of algebras) | both, of course, arbitrarily parameterised. Aiming at the development of an institutionindependent framework, we decided to omit from our considerations yet another level of objects involved, namely that of algebra components (such as data values and operations on them). In particular institutions, however, it may be interesting to explicitly consider this level as well, and to intermix constructs for dealing with this level with those for the other two levels mentioned above. This would lead to entities such as algebras parametric on data values, speci cations parameterised by functions on data, functions from algebras and speci cations to data values, etc. Just as the kernel ASL-like speci cation formalism it builds on, the presented system is too lowlevel to be directly useful in practice. We view it primarily as a kernel to be used as a semantic foundation for the development of more user-friendly speci cation languages. Easier to use notations can be devised, with their semantics de ned by translation into the formalism of Section 7. The material in Section 7 is more tentative than that in the remainder of the paper, and clearly some of the details of the design of the speci cation formalism deserve further consideration. The choice of operations used to build simple speci cations is not essential; we have chosen here those of ASL (derive, translate, etc.) but any reasonably expressive set of operations would su ce, and most of the subsequent technical development would require little or no modi cation. Adding e.g. an intersection operation (dual to union) to the present system would be completely unproblematic. A less straightforward extension would be to add recursion for building speci cations as in SW 83], ST 88a]: for a parameterised speci cation P , x P would be a speci cation denoting the greatest xed point of the (monotone) function P ] on classes of objects. Yet another thing to consider is the possible bene ts of making the ( )] and ( )y operators of Sections 4.2 explicitly available. It is not clear how the system of rules in Section 7.3 could be enriched to cope with these additions though. The presented system provides an appropriate foundation for the Extended ML speci cation language and program development methodology as presented in ST 89]. Indeed, one of the main stimuli to write this paper was our inability to express the semantics of the current version of Extended ML directly in terms of the kernel speci cation-building operations in ASL: Extended ML functor speci cations are speci cations of parametric objects, and these were not present in ASL. The task of writing out a complete semantics of Extended ML in terms of the speci cation formalism presented here remains to be done. We expect that some technicalities, like those which arise in connection with ML type inheritance, will cause the same problems as in ST 89]. Some others, like the use of behavioural equivalence and the concept of functor stability in the Extended ML methodology, although directly related to the abstract operation in the formalism presented here, require further study in this more general framework. Finally, properties of ML functors such as persistency, which cause di culties in other speci cation formalisms, will be easy to express here. One of the interesting possibilities the system presented in Section 7 o ers is that it incorporates the concept of speci cation re nement, cf. ST 88b]. Namely, we can de ne SP > SP 0 (read: SP 0 is a 42 re nement of SP | this is equivalent to SP id > SP 0 in the notation of Section 6) as SP 0 : Spec(SP ). This also covers re nements of speci cations of (higher-order) parametric algebras, due to the following derivable rule: X : SP ] SP 0 > SP 00 (i.e. SP 00 : Spec(SP 0)) X :SP: SP 0 > X :SP: SP 00 (i.e. X :SP: SP 00 : Spec( X :SP: SP 0)) We can also \internalize" SP > hSP1; : : :; SPni, for example as : X1:SP1: Xn:SPn : SP . The consequences of such an internalisation of development steps seem worth exploring. This was one of the ideas underlying the design of the Spectral speci cation language KS 91] which can be seen as a higher-level and more user-friendly version of a subset of the formalism presented here. The formal properties of the system presented in Section 7 need much further study. For example, it seems that the \cut" rule should be admissible (although not derivable) in the remainder of the system. The standard properties of -reduction, such as the Church-Rosser property and termination (on well-formed objects) should be carefully proven, probably by reference to the analogous properties of the usual typed -calculus. For example, the termination property of -reduction on the well-formed objects of the language should follow easily from the observation that the Erase function introduced in Section 7.4 preserves -reduction, which allows us to lift the corresponding property of the usual typed -calculus to our formalism. The system is incomplete, as pointed out earlier. It would be useful to identify all the sources of this incompleteness, for example by characterising an interesting subset of the language for which the system is complete. One line of research which we have not followed (as yet) is to try to encode the formalism we present here in one of the known type theories (for example, Martin-Lof's system NPS 90], the calculus of constructions CH 88] or LF HHP 87]). It would be interesting to see both which of the features of the formalism we propose would be di cult to handle, as well as which of the tedious proofs of some formal properties of our formalism (cf. the proofs sketched for Theorems 7.9 and 7.11 in ST 91a]) would turn out to be available for free under such an encoding. Our attention has recently been drawn to certain intriguing similarities between some of the rules presented in Section 7.3 and those in the paper \Structural subtyping and the notion of power type" by Luca Cardelli in Proc. 15th ACM Symp. on Principles of Programming Languages, San Diego, 70{79 (1988). Among other things, the Spec operator here is closely related to Cardelli's Power type-formation operator, our \cut" rule (R11) corresponds to his Power elimination rule, and our rule (R3) corresponds to his Power subtyping rule. Acknowledgements: Thanks to David Aspinall, Jan Bergstra, Jordi Farres, John Fitzgerald, MarieClaude Gaudel, Joseph Goguen, Claudio Hermida, Cli Jones, Stefan Kahrs, Ed Kazmierczak, Bernd Krieg-Bruckner, Jacek Leszczylowski, Fernando Orejas, Lincoln Wallen and Martin Wirsing for interesting discussions and suggestions on this topic. Thanks to the referees for comments on an earlier version of the paper. This research was supported by the University of Edinburgh, the University of Bremen, the Technical University of Denmark, the University of Manchester, and by grants from the Polish Academy of Sciences, the (U.K.) Science and Engineering Research Council, ESPRIT, and the Wolfson Foundation. Note added in proof. 9 References Note: LNCS n = Springer Lecture Notes in Computer Science, Volume n ] 43 Bau 85] Bauer, F.L. et al (the CIP language group). The Wide Spectrum Language CIP-L. LNCS 183 (1985). Bid 88] Bidoit, M. The strati ed loose approach: a generalization of initial and loose semantics. Recent Trends in Data Type Speci cation, Selected Papers from the 5th Workshop on Speci cation of Abstract Data Types, Gullane, Scotland. LNCS 332, 1{22 (1988). BKS 88] Borzyszkowski, A.M., Kubiak, R. and Sokolowski, S. A set-theoretic model for a typed polymorphic -calculus. Proc. VDM-Europe Symp. VDM { The Way Ahead, Dublin. LNCS 328, 267{298 (1988). BG 80] Burstall, R.M. and Goguen, J.A. The semantics of CLEAR, a speci cation language. Proc. of Advanced Course on Abstract Software Speci cation, Copenhagen. LNCS 86, 292{332 (1980). Bir 48] Birkho , G. Lattice Theory. American Mathematical Society (1948). BT 83] Blikle, A. and Tarlecki, A. Naive denotational semantics. Information Processing 83, Proc. IFIP Congress'83, Paris, ed. R. Mason, 345{355, North-Holland 1983. Coh 81] Cohn, P.M. Universal Algebra. Reidel (1981). Con 86] Constable, R.L. et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall (1986). CH 88] Coquand, T. and Huet, G. The calculus of constructions. Information and Computation 76, 95{120 (1988). Ehr 82] Ehrich, H.-D. On the theory of speci cation, implementation, and parametrization of abstract data types. Journal of the Assoc. for Computing Machinery 29, 206{227 (1982). EM 85] Ehrig, H. and Mahr, B. Fundamentals of Algebraic Speci cation I: Equations and Initial Semantics. Springer (1985). ETLZ 82] Ehrig, H., Thatcher, J.W., Lucas, P. and Zilles, S.N. Denotational and initial algebra semantics of the algebraic speci cation language LOOK. Report 84-22, Technische Universitat Berlin (1982). Far 92] Farres-Casals, J. Veri cation in ASL and Related Speci cation Languages. Ph.D. thesis, report CST-92-92, Dept. of Computer Science, Univ. of Edinburgh (1992). FJ 90] Fitzgerald, J.S. and Jones, C.B. Modularizing the formal description of a database system. Proc. VDM'90 Conference, Kiel. Springer LNCS 428 (1990). Gan 83] Ganzinger, H. Parameterized speci cations: parameter passing and implementation with respect to observability. Trans. Prog. Lang. Syst. 5, 318{354 (1983). GM 88] Gaudel, M.-C. and Moineau, T. A theory of software reusability. Proc. 2nd European Symp. on Programming, Nancy. LNCS 300, 115{130 (1988). Gog 84] Goguen, J.A. Parameterized programming. IEEE Trans. Software Engineering SE-10, 528{ 543 (1984). GB 84] Goguen, J.A. and Burstall, R.M. Introducing institutions. Proc. Logics of Programming Workshop, Carnegie-Mellon. LNCS 164, 221{256 (1984). GHW 85] Guttag, J.V., Horning, J.J. and Wing, J. Larch in ve easy pieces. Report 5, DEC Systems Research Center, Palo Alto, CA (1985). HHP 87] Harper, R., Honsell, F. and Plotkin, G. A framework for de ning logics. Proc. 2nd IEEE Symp. on Logic in Computer Science, Cornell, 194{204 (1987). 44 KS 91] Krieg-Bruckner, B. and Sannella, D. Structuring speci cations in-the-large and in-the-small: higher-order functions, dependent types and inheritance in Spectral. Proc. Colloq. on Combining Paradigms for Software Development, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Brighton. Springer LNCS 494, 313{336 (1991). LL 88] Lehmann, T. and Loeckx, J. The speci cation language of OBSCURE. Recent Trends in Data Type Speci cation, Selected Papers from the 5th Workshop on Speci cation of Abstract Data Types, Gullane, Scotland. LNCS 332, 131{153 (1988). MacQ 86] MacQueen, D.B. Modules for Standard ML. in: Harper, R., MacQueen, D.B. and Milner, R. Standard ML. Report ECS-LFCS-86-2, Univ. of Edinburgh (1986). MMMS 87] Meyer, A.R., Mitchell, J.C., Moggi, E. and Statman, R. Empty types in polymorphic lambda calculus. Proc. 14th ACM Symp. on Principles of Programming Languages, 253{262; revised version in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990), 273{284. Mos 89a] Mosses, P. Uni ed algebras and modules. Proc. 16th ACM Symp. on Principles of Programming Languages, Austin, 329{343 (1989). Mos 89b] Mosses, P. Uni ed algebras and institutions. Proc. 4th IEEE Symp. on Logic in Computer Science, Asilomar, 304{312 (1989). NPS 90] Nordstrom, B., Petersson, K. and Smith, J.M. Programming in Martin-Lof's Type Theory: An Introduction. Oxford Univ. Press (1990). San 91] Sannella, D. Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Re nement, Hursley Park. Springer BCS Workshop series (1991). SST 90] Sannella, D., Sokolowski, S. and Tarlecki, A. Toward formal development of programs from algebraic speci cations: parameterisation revisited. Report 6/90, FB Informatik, Universitat Bremen (1990). ST 85] Sannella, D. and Tarlecki, A. Program speci cation and development in Standard ML. Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, 67{77 (1985). ST 87] Sannella, D. and Tarlecki, A. On observational equivalence and algebraic speci cation. J. Comp. and Sys. Sciences 34, 150{178 (1987). ST 88a] Sannella, D. and Tarlecki, A. Speci cations in an arbitrary institution. Information and Computation 76, 165{210 (1988). ST 88b] Sannella, D. and Tarlecki, A. Toward formal development of programs from algebraic speci cations: implementations revisited. Acta Informatica 25, 233{281 (1988). ST 89] Sannella, D. and Tarlecki, A. Toward formal development of ML programs: foundations and methodology. Report ECS-LFCS-89-71, Laboratory for Foundations of Computer Science, Dept. of Computer Science, Univ. of Edinburgh (1989); extended abstract in Proc. Colloq. on Current Issues in Programming Languages, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Barcelona. LNCS 352, 375{389 (1989). ST 91a] Sannella, D. and Tarlecki, A. A kernel speci cation formalism with higher-order parameterisation. Proc. 7th Intl. Workshop on Speci cation of Abstract Data Types, Wusterhausen. Springer LNCS 534, 274{296 (1991). ST 91b] Sannella, D. and Tarlecki, A. Extended ML: past, present and future. Proc. 7th Intl. Workshop on Speci cation of Abstract Data Types, Wusterhausen. Springer LNCS 534, 297{322 (1991). 45 ST 92] Sannella, D. and Tarlecki, A. Toward formal development of programs from algebraic speci cations: model-theoretic foundations. Proc. Intl. Colloq. on Automata, Languages and Programming, Vienna. Springer LNCS 623, 656{671 (1992). SW 83] Sannella, D. and Wirsing, M. A kernel language for algebraic speci cation and implementation. Proc. Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. LNCS 158, 413{427 (1983). Sch 87] Schoett, O. Data abstraction and the correctness of modular programming. Ph.D. thesis, report CST-42-87, Dept. of Computer Science, Univ. of Edinburgh (1987). Sok 90] Sokolowski, S. Parametricity in algebraic speci cations: a case study. Draft report, Institute of Computer Science, Polish Academy of Sciences, Gdansk (1990). Tar 92] Tarlecki, A. Modules for a model-oriented speci cation language: a proposal for MetaSoft. Proc. 4th European Symp. on Programming, Rennes. Springer LNCS 582, 451{472 (1992). Vo 85] Vo , A. Algebraic speci cations in an integrated software development and veri cation system. Ph.D. thesis, Universitat Kaiserslautern (1985). Wir 86] Wirsing, M. Structured algebraic speci cations: a kernel language. Theor. Comp. Science 42, 123{249 (1986). 46