Under consideration for publication in Math. Struct. in Comp. Science

Observational Interpretation of Casl Specifications

M I C H E L B I D O I T^{†}, D O N A L D S A N N E L L A^{‡} and A N D R Z E J T A R L E C K I^{§}

† Laboratoire Spécification et Vérification, CNRS & ENS de Cachan, France

Website: www.lsv.ens-cachan.fr/~bidoit/

‡ Laboratory for Foundations of Computer Science, University of Edinburgh, UK

Website: homepages.inf.ed.ac.uk/dts/

§ Institute of Informatics, Warsaw University, and Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland

Website: www.mimuw.edu.pl/~tarlecki/

Received 12 September 2006; Revised 15 June 2007

The way that refinement of individual “local” components of a specification relates to development of a “global” system from a specification of requirements is explored. Observational interpretation of specifications and refinements add expressive power and flexibility while bringing in some subtle problems. Our study of these issues is carried out in the context of Casl architectural specifications. We introduce a definition of observational equivalence for Casl models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.

1. Introduction

There has been a great deal of work in the algebraic specification tradition on formalizing the rather intuitive and appealing idea of program development by stepwise refinement, including (Ehrig et al. 1982; Ganzinger 1983; Schoett 1987; Sannella and Tarlecki 1988b); for a survey, see (Ehrig and Kreowski 1999). There are many issues that make this a difficult problem, and some of them are rather subtle, one example being the relationship between specification structure and program structure, and another being the tradeoff between the expressive power of a specification formalism and the ease of reasoning about specifications. Significant complications result when “observational” or “behavioural” aspects of specifications are considered, whereby the definition of correctness takes into account only the results of those computations that can be directly observed. An overview that covers most of our own contributions is (Sannella and Tarlecki 1997), with some more recent work addressing the problem of how to prove correctness of refinement steps (Bidoit and Hennicker 1998; Bidoit and Hennicker 2006), the design of a convenient formalism for writing specifications (Bidoit, Sannella and Tarlecki 2002a; Astesiano et al. 2002; CoFI 2004), and applications to data refinement in typed λ-calculus (Honsell et al. 2000).

A new angle that we explore here is the “global” effect of refining individual “local” components of a specification. This involves a well-known technique from algebraic specification, namely the use of pushouts of signatures and amalgamation of models to build large systems by composition of separate interrelated components. The situation becomes considerably more subtle when observational interpretation of specifications and refinements is brought into the picture.

Part of the answer has already been provided, the main references being Schoett’s thesis (Schoett 1987; Schoett 1990) and our work on formal development in the Extended ML framework (Sannella and Tarlecki 1989); the general ideas go back at least to (Hoare 1972). We have another look at these issues here, in the context of the Casl specification formalism (Astesiano et al. 2002; CoFI 2004) and in particular, its architectural specifications (Bidoit, Sannella and Tarlecki 2002a). Architectural specifications, for describing the modular structure of software systems, are probably the most novel feature of Casl. We view them here as a means of making complex refinement steps, by defining a construction to be used to build the overall system from implementations of individually-specified units; these may include parametrized units that contribute to this construction.

This paper combines and expands on previous work reported in (Bidoit, Sannella and Tarlecki 2002a; Bidoit, Sannella and Tarlecki 2002b; Bidoit, Sannella and Tarlecki 2004; Baumeister et al. 2004; Schröder et al. 2005). It interweaves three strands. The first strand (Sects. 2 and 5) recalls the basic semantic concepts of Casl and introduces observational equivalence for Casl models and the induced observational interpretation of Casl basic and structured specifications. In contrast to (Bidoit, Sannella and Tarlecki 2002b), true Casl models are considered rather than standard many-sorted total algebras.

A second strand (Sects. 3 and 6) explores the use of local constructions in an arbitrary global context, and its interaction with an observational view of requirements specifications. In particular, stability and observational correctness of constructions on Casl models are treated, and practical local criteria to establish both properties are formulated.

The final strand (Sects. 4 and 7) provides a careful analysis of the semantics of Casl architectural specifications, taking account of the fact that amalgamability is not ensured for Casl models and linking with the other strands to provide such specifications with an observational semantics. Key invariant properties of the semantics are precisely formulated and proved.

Due to space considerations we do not deal with full-blown Casl as defined in (Mosses 2004), but the addition of unit definitions to the treatment in (Bidoit, Sannella and Tarlecki 2002b) together with a proper account of dependencies between units means that the extension to full Casl would be routine. The analysis of invariants linking the static semantics and model semantics of architectural specifications in Sect. 4 provides essential insight into the semantics of full Casl that was implicit in (Baumeister et al. 2004); this reiterates Thm. 2 in (Schröder et al. 2005) and provides a basis for an analogous treatment of the observational case in Sect. 7.

An orthogonal view of the structure of this paper is that Sects. 2–4 present a standard treatment of Casl basic and structured specifications, local constructions and their use in a global context, and Casl architectural specifications; a comprehensive observational treatment is then given in Sects. 5–7. An example in Sect. 8, based on one in (Bidoit, Sannella and Tarlecki 2004), provides a concrete illustration of some of the points that arise.

Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications (Baumeister et al. 2004) with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.

2. Casl Institution and Specifications

A basic assumption underpinning algebraic specification and derived approaches to software specification and development is that programs are modelled as algebras (of some kind) with their “types” captured by algebraic signatures (again, adapted as appropriate). Then specifications include axioms describing the required properties. This leads to quite a flexible framework, which can be tuned as desired to cope with various programming features of interest by selecting the appropriate variation of algebra, signature and axiom. This flexibility has been formalized via the notion of institution (Goguen and Burstall 1992) and related work on the theory of specifications and formal program development (Sannella and Tarlecki 1988a; Sannella and Tarlecki 1997; Bidoit and Hennicker 1993).

Let us recall that an institution defines a notion of signature together with for any signature Σ, a set of Σ-sentences, a class of Σ-models equipped with homomorphisms, and a satisfaction relation between Σ-models and Σ-sentences. Moreover, signatures come equipped with signature morphisms, forming a category. Any signature morphism induces a translation of sentences and a translation of models (the latter going in the opposite direction to the morphism). All this can be expressed very concisely using the language of category theory: we require a category Sig, a functor Sen : Sig → Set, a (contravariant) functor Mod : Sig^{op} → Cat, and a family of binary relations ⟨⊧_{Σ} ⊆ |Mod(Σ)| × Sen(Σ)⟩_{Σ∈|Sign|}. The only semantic requirement is that when we change signatures using a signature morphism, the induced translations of sentences and of models preserve the satisfaction relation.

By now it is standard to base work on specification languages and formal program development on the notion of an institution, so that a clear separation between logicdependent details and general logic-independent aspects of the work can be achieved. We follow this below, recalling the logical system of Casl (Bidoit and Mosses 2004).

Casl is an algebraic specification language for describing Casl models: many-sorted algebras with subsorts, partial and total operations, and predicates. Casl models are classified by Casl signatures, which give sort names (with their subsorting relation), partial and total operation names, and predicate names, together with profiles of operations and predicates. In Casl models, subsorts and supersorts are linked by implicit subsort embeddings that are required to compose with each other and to be compatible with operations and predicates with the same names.

Recalling (and slightly simplifying) some technical detail from (Baumeister et al. 2004): a Casl signature is a tuple Σ = (S, TF , PF , P, ≤), where S is a set of sort names, TF = ⟨TF_{ws}⟩_{ws∈S^{+}} and PF = ⟨PF_{ws}⟩_{ws∈S^{+}} are families of total and partial, respectively, operation names, indexed by their profiles (which consist of their arity w ∈ S^{∗} and result sort s ∈ S), P = ⟨P_{w}⟩_{w∈S^{∗}} is a family of predicate names, indexed by their arities, and ≤ is a subsorting preorder on S (a relation that is reflexive and transitive). For simplicity, we bluntly assume that no overloading is allowed, that is, that all the sets in TF , PF , and P are mutually disjoint^{1}. We write f: s_{1} × ⋯ × s_{n} → s when s_{1}, …, s_{n}, s ∈ S and f ∈ TF_{s_{1}...s_{n}s}; similar notation is used for partial operation names and for predicate symbols. If n = 0 then f is a constant and we write f: s. For Casl signatures Σ = (S, TF , PF , P, ≤) and Σ′ = (S′, TF′, PF′, P′, ≤′), a morphism between them, written σ : Σ → Σ′, maps sort names in S to sort names in S′ so that the subsorting preorder is preserved, operation names in TF ∪ PF to operation names in TF′ ∪ PF′ so that their totality and profiles are preserved, and predicate names in P to predicate names in P′ so that their arities are preserved. This yields a category Sig of Casl signatures and their morphisms with the obvious identities and component-wise composition.

Given a Casl signature Σ = (S, TF , PF , P, ≤), we define its expansion to a manysorted signature Σ^{#} that retains the set of sorts S and includes the operation and predicate names from TF , PF and P, adding for all s ≤ s′ in Σ, a new total operation name em^{s≤s′}: s → s′ for subsort embedding, a new partial operation name pr^{s≤s′}: s′ → s for subsort projection, and a new predicate name in^{s≤s′}: s′ for subsort membership. Note that ( )^{#} extends to signature morphisms in an obvious way.

Now, a Casl model over the Casl signature Σ = (S, TF , PF , P, ≤) is a structure M over the signature Σ^{#}, which consists of a carrier set |M|_{s} for each sort s ∈ S, a (partial) function f_{M}: |M|_{s_{1}} × ⋯ × |M|_{s_{n}} → |M|_{s} for each operation name f: s_{1} × ⋯ × s_{n} → s in Σ^{#} (with f_{M} being total for total operation names f) and a relation p_{M} ⊆ |M|_{s_{1}} × ⋯ × |M|_{s_{n}} for each predicate name p: s_{1} × ⋯ × s_{n}, such that for all s ≤ s′ in Σ, the subsort embedding em_{M}^{s≤s′}: |M|_{s} → |M|_{s′} is injective, the subsort projection pr_{M}^{s≤s′}: |M|_{s′} → |M|_{s} is defined exactly on the image of em_{M}^{s≤s′} as its inverse, and the subsort membership predicate in_{M}^{s≤s′} ⊆ |M|_{s′} holds exactly on the image of em_{M}^{s≤s′}. Moreover, we require that em_{M}^{s≤s} is the identity for s ∈ S, and that the embeddings compose, that is, if s ≤ s′ ≤ s′′ then em_{M}^{s≤s′′} is the composition of em_{M}^{s≤s′} and em_{M}^{s′≤s′′}.

This yields the class of Casl Σ-models, which form a category Mod(Σ) with homomorphisms between Σ^{#}-structures defined as usual, as maps that preserve predicates as well as the definedness and values of operations. A homomorphism is strong if it also reflects the predicates and the definedness of operations. Given a Casl Σ-model M, a

1 This assumption is unrealistic in practical examples, especially when subsorting is involved; Casl deals with this properly, imposing only a considerably weaker version of this restriction. The issues that arise are irrelevant for the topic of this paper.

submodel is any Casl Σ-model N with carriers of N included in those of M such that the inclusion function |N| ↪ |M| is a strong homomorphism, cf. closed subalgebras in (Burmeister 1986).

As expected, kernels of homomorphisms between Casl models are congruences: equivalence relations on model carriers closed under operations when defined in the model (this also applies to the subsort embeddings and projections). Kernels of strong homomorphisms are strong congruences: these are congruences that in addition preserve predicates and definedness of operations. Given any Casl Σ-model M and congruence ≃ on it, the quotient of M by ≃ is defined as the quotient of M as a Σ^{#}-structure by ≃; it is easy to check that the usual definition yields a Σ^{#}-structure which is a Casl Σ-model, and that the natural quotient homomorphism is strong whenever the congruence ≃ is strong.

Any Casl signature morphism σ: Σ → Σ′ determines a reduct functor from Mod(Σ′) to Mod(Σ), where for any Σ′-model M′ ∈ |Mod(Σ′)|, its reduct M′ _{σ} ∈ |Mod(Σ)| is defined as the σ^{#}-reduct of the (Σ′)^{#}-structure M′: any sort, operation or predicate name ν in Σ^{#} gets the same interpretation in M′ _{σ} as σ^{#}(ν) has in M′. Similarly for homomorphisms, and for arbitrary relations between carriers of Casl models. This completes the definition of a functor Mod : Sig^{op} → Cat.

It is easy to check that the category Sig of Casl signatures is (finitely) cocomplete, with colimits of diagrams given in the expected, component-wise way. Note in particular that the subsort preorder in the colimit signature is the transitive closure of the union of the images of the subsort preorders of the signatures in the diagram under the colimit injections. We will assume that some standard construction of pushouts in Sig is given.

Colimits in Sig offer a rudimentary way of putting together Casl signatures and basic specifications over them (see below), very much as in the standard algebraic framework (Ehrig and Mahr 1985). When it comes to model theory though, things are more difficult, since Casl does not ensure that the amalgamation property holds.

Definition 2.1 (Amalgamation). A pushout in the category of Casl signatures:

[figure: Σ; Σ_{1}; Σ′; Σ′_{1}; γ; ι; ι′; γ′]

ensures amalgamability if for all models M_{1} ∈ |Mod(Σ_{1})| and M′ ∈ |Mod(Σ′)| such that M_{1} _{γ} = M′ _{ι} there exists a unique model M′_{1} ∈ |Mod(Σ′_{1})| such that M′_{1} _{ι′} = M_{1} and M′_{1} _{γ′} = M′. We sometimes write M_{1} ⊕ M′ for such a unique M′_{1} and call it the amalgamation of M_{1} and M′, when the pushout is clear from the context.

When the signature morphism ι is given and the pushout as above ensures amalgamability, we will refer to the morphism γ as admissible (cf. Def. 3.3 below).

It is worth stressing that pushouts of Casl signature morphisms between signatures with no proper subsorts (i.e., the subsorting preorders are identities) always ensure amalgamability. The potential problems are caused by the built-in requirements of uniqueness and composability of subsort embeddings in Casl models. The simplest example of a pushout that does not ensure amalgamability is when Σ contains just two sorts, and both Σ_{1} and Σ′ expand Σ by adding a new subsort relationship between the two sorts. The pushout signature then coincides with Σ_{1} = Σ′ (and so allows for one subsort embedding between the two sorts), and two models over Σ_{1} and Σ′ with common Σ-reduct amalgamate only if they happen to share the same subsort embedding. Perhaps surprisingly, the problem whether a pushout (or more generally, a colimit) ensures amalgamability is in general undecidable, but a number of effective algorithms to determine this in various practically relevant cases can be given. However, we do not know any easy syntactic condition that would ensure amalgamability without excluding some cases that naturally arise in practical specifications. For instance, requiring that ι and γ in the diagram above do not introduce new subsorting relationships between sorts from Σ is not sufficient. To see this, consider Σ with just two independent sorts, Σ_{1} which adds a new common subsort for them, and Σ′ which add a new common supersort for them. Then the resulting pushout does not ensure amalgamability. We refer to (Schröder et al. 2001; Klin et al. 2001; Schröder et al. 2005) for further examples and a more complete study of amalgamability in Casl. Here, we just guard any use of amalgamation with a requirement that the relevant pushout ensures amalgamability.

In the framework of Casl, if a pushout ensures amalgamability (of Casl models, as above) then it also ensures amalgamability of homomorphisms:

Lemma 2.2. Suppose that the following pushout

[figure: Σ; Σ_{1}; Σ′; Σ′_{1}; γ; ι; ι′; γ′]

ensures amalgamability. Then for all homomorphisms h_{1}: M_{1} → N_{1} in Mod(Σ_{1}) and h′: M′ → N′ in Mod(Σ′) such that h_{1} _{γ} = h′ _{ι} there exists a unique homomorphism h′_{1}: M′_{1} → N′_{1} in Mod(Σ′_{1}) such that h′_{1} _{ι′} = h_{1} and h′_{1} _{γ′} = h′. Moreover, h′_{1} is strong if both h_{1} and h′ are strong.

Proof. Let M′_{1} = M_{1} ⊕M′ and N′_{1} = N_{1} ⊕N′ (they are well-defined, since the pushout ensures amalgamability). For each sort s_{1} in Σ_{1}, put (h′_{1})_{ι′(s_{1})} = (h_{1})_{s_{1}}; for each sort s′ in Σ′, put (h′_{1})_{γ′(s′)} = (h′)_{s′}. By the construction of pushouts in Sig, this yields a well-defined family of functions (h′_{1})_{s}: |M′_{1}|_{s} → |N′_{1}|_{s}, for sorts s in Σ′_{1}. The required compatibility with the predicates and operations of the form (ι′)^{#}(f_{1}), for f_{1} in Σ_{1}^{#}, follows from the compatibility of h_{1} with the predicates and operations in Σ_{1}^{#}; similarly for the predicates and operations of the form (γ′)^{#}(f′) for f′ in (Σ′)^{#}. Consider then a subsort embedding in (Σ′_{1})^{#}. Since the subsort relation in Σ′_{1} is the transitive closure of the union of the images of the subsort relations in Σ_{1} and Σ′ under ι′ and γ′, respectively, the embedding is a composition of embedding operations of the forms considered above — and so compatibility follows by an easy induction. Similarly for subsort projections in Σ′_{1}, and then for the subsort membership predicates (which are defined as the domains of the corresponding subsort projections).

Given a Casl signature Σ, we assume the usual definition of a first-order formula (with quantification and the usual logical connectives) built over atomic formulae which include strong and existential equalities, definedness formulae and predicate applications, over the many-sorted signature Σ^{#}, and its satisfaction in a Σ^{#}-structure. Adding so-called generation constraints as special, non-first-order sentences, yields the set of Casl Σsentences, written Sen(Σ). Given a Casl signature morphism σ: Σ → Σ′, the translation of any Σ-sentence φ ∈ Sen(Σ) is defined as usual, and we write it as σ(φ), see (Baumeister et al. 2004). This defines a functor Sen : Sig → Set.

As usual for first-order logic, satisfaction is defined for the more general case of formulae with free variables; we write M[v] ⊧_{Σ} φ to state that the Σ-formula φ with free variables in a set X holds in the Σ-model M under the valuation v: X → |M|. The signature subscript in ⊧_{Σ} is usually left implicit. The notation (t)_{M[v]} is used to denote the value of a term t with variables in X in the model M under the valuation v: X → |M|; this may be undefined, when the term involves partial operations. Satisfaction of formulae and evaluation of terms only depend on the valuation of their free variables. We drop the valuation v in this notation for closed terms (terms with no variables) and sentences (formulae with no free variables). The satisfaction of sentences is preserved under signature morphisms: for any σ: Σ → Σ′, M′ ∈ |Mod(Σ′)| and φ ∈ Sen(Σ), we have

M′ _{σ} ⊧ φ ⟺ M′ ⊧ σ(φ)

We consider Casl formulae built over the usual algebraic terms only, so in particular Casl conditional terms are excluded (they can be easily eliminated in formulae anyway, see (CoFI 2004)).

We introduce a more general form of conditional terms, as follows, but without allowing them in formulae. Given a Casl signature Σ, a conditional term of sort s with variables in X is of the form c = ⟨(ϕ_{i}, t_{i})⟩_{i≥0}, where for i ≥ 0, ϕ_{i} are formulae with variables in X, and t_{i} are terms of sort s with variables in X. Given a Σ-model M and a valuation v: X → |M|, the value c_{M[v]} of such a conditional term c is (t_{k})_{M[v]} for the least k ≥ 0 such that M[v] ⊧ ϕ_{k}, or is undefined if no such k ≥ 0 exists. Note that the infinitary unfolding of any recursive definition can be captured by such a conditional term. Therefore we use these conditional terms to model arbitrary computations, even though they go well beyond what programming languages offer: arbitrary formulae are used as conditions without regard to decidability, the sequence of conditions and terms need not even be recursively enumerable, etc. Some of this generality will be excluded by requirements arising from discussion in Sections 5 and 6.1.

We use these conditional terms to generalize derived signature morphisms (Goguen, Thatcher and Wagner 1978). A derived signature morphism δ: Σ → Σ′ maps partial operation symbols f: s_{1} × … × s_{n} → s in Σ to conditional Σ′-terms of sort δ(s) with variables {x_{1}: δ(s_{1}), …, x_{n}: δ(s_{n})}. Evidently, such a derived signature morphism δ: Σ → Σ′ still determines a reduct function _{δ} mapping Σ′-models to Σ-models. In general this does not extend to a reduct functor between model categories, since values of conditional terms with arbitrary conditions need not be preserved by homomorphisms (but see the comment following Lemma 5.5).

The basic level of Casl includes declarations to introduce components of signatures and axioms to give properties that characterize models of a specification. Consequently, a basic Casl specification SP amounts to a definition of a signature Σ and a set of axioms Φ ⊆ Sen(Σ). It denotes the class [[SP]] ⊆ |Mod(Σ)| of SP-models, which are those Σ-models that satisfy all the axioms in Φ:

[[SP]] = {M ∈ |Mod(Σ)| | M ⊧ Φ}.

Apart from basic specifications as above, Casl provides ways of building complex specifications out of simpler ones by means of various structuring constructs. These include translation, hiding, union, and both free and loose forms of extension. Generic specifications and their instantiations with pushout-style semantics (Burstall and Goguen 1980; Ehrig and Mahr 1985) are also provided. Structured specifications built using these constructs are given a compositional semantics where each specification SP determines a signature Sig[SP] and a class [[SP]] ⊆ |Mod(Sig[SP])| of models. Most of the details, given in (Baumeister et al. 2004), are irrelevant for the purposes of this paper. It is enough to know the following: for any specification SP and signature morphism σ: Sig(SP) → Σ′, we write SP with σ for the translation of SP along σ, with semantics given by Sig[SP with σ] = Σ′ and [[SP with σ]] = {M′ ∈ |Mod(Σ′)| | M′ _{σ} ∈ [[SP]]}, and for any two specifications SP_{1} and SP_{2} with common signature, we write SP_{1} and SP_{2} for their union, with semantics given by Sig[SP_{1} and SP_{2}] = Sig[SP_{1}] = Sig[SP_{2}] and [[SP_{1} and SP_{2}]] = [[SP_{1}]] ∩ [[SP_{2}]]. Note that union in Casl generalizes this by allowing Sig[SP_{1}] ≠ Sig[SP_{2}].

3. Software Components and Their Correctness

The intended use of Casl, as of any such specification formalism, is to specify programs. Each Casl specification should determine a class of programs that correctly realize the specified requirements. To fit this into the formal view of Casl specifications, programs must be written in a programming language having a semantics which assigns to each program its denotation as a Casl model.^{2} Then each program P determines a Casl signature Sig[P] and a model [[P]] ∈ |Mod(Sig[P])|. Any specification SP is then a description of its admissible realizations: a program P is a (correct) realization of SP if Sig[P] = Sig[SP] and [[P]] ∈ [[SP]].

Let us now consider component-based systems, that is, systems obtained by assembling components, rather than “monolithic” programs. We take a rather restrictive view of components, namely software components (understood as pieces of code) in contrast with

2 This may be rather indirect, and in general involves a non-trivial abstraction step. It has not yet been attempted for any real programming language, but see (Schröder and Mossakowski 2002) for an outline of how this could be done for Haskell. See also the pre-Casl work on Extended ML (Kahrs, Sannella and Tarlecki 1997), and see Larch (Guttag and Horning 1993) for another attempt to link a specification language with various programming languages.

system components (understood as self-contained processors with their own hardware and software interacting with each other and the environment by exchanging messages across linking interfaces). However, our view is consistent with the best accepted definition in the software industry, see (Szyperski 1998): a (software) component is an independentlydeployable unit of composition with contractually specified interfaces and fully explicit context dependencies.

To capture this, we will consider that a software component ΔP determines a “parameter” signature, say Σ, corresponding to the symbols required by the component, and a “result” signature, say Σ′, corresponding to the symbols provided by the component, together with a signature morphism ι: Σ → Σ′ relating the “parameter” signature to the “result” signature. Thereby ι: Σ → Σ′ corresponds to the (syntactic part of the) interface of the software component.

Then the software component ΔP determines a function F = [[ΔP]] from Casl Σmodels to Casl Σ′-models. This function may be partial, see below. When assembled with (applied to) a sub-system P (determining a Casl signature Sig[P] = Σ and a model [[P]] ∈ |Mod(Σ)|), the software component ΔP “extends” P to a larger system, say ΔP (P), with signature Sig[ΔP (P)] = Σ′, determining a Casl model [[ΔP (P)]] ∈ |Mod(Σ′)|. It is intuitively clear that the software component “preserves” the sub-system it is applied to, so [[ΔP (P)]] _{ι} = [[P]].

Thus a software component ΔP determines a semantic object F called a local construction according to the definition below. Since software components preserve their arguments, we assume that such constructions are persistent: the argument of a construction is always fully included in its result, without modification^{3} — note that this assumption holds for all constructions that can be declared and specified in Casl, see Sect. 4. In fact, we generalize Casl somewhat by considering arbitrary signature morphisms rather than just inclusions.

Definition 3.1 (Local construction). Given a signature morphism ι: Σ → Σ′, a local construction along ι is a persistent partial function F: |Mod(Σ)| ⇀ |Mod(Σ′)| (for each M ∈ dom(F), F (M) _{ι} = M). We write Mod(Σ⟶^{ι}Σ′) for the class of all local constructions along ι.

We will not dwell here on how particular local constructions are defined. Free functor semantics for parametrized specifications is one way to proceed, with the persistency requirement giving rise to additional proof obligations (Ehrig and Mahr 1985). Perhaps closer to ordinary programming, any “definitional” derived signature morphism δ: Σ′ → Σ that defines Σ′-components in terms of Σ-components naturally gives rise to a local

3 Otherwise we would have to explicitly indicate “sharing” between the argument and result of each construction, and explain how such sharing is preserved by the various ways of putting together constructions, as was painfully spelled out in (Sannella and Tarlecki 1989). If necessary, superfluous components of models constructed using persistent constructions can be discarded at the end using the reduct along a signature inclusion.

construction, since the induced reduct function _{δ}: |Mod(Σ)| → |Mod(Σ′)| is a local construction along a signature morphism ι: Σ → Σ′ whenever ι;δ = id_{Σ}.^{4}

Of course we are interested in specifications of software components, that is, in “semantic” specifications of the parameter required by the component and of its result (and not only in the “syntactic” specification of its interface given by ι: Σ → Σ′). Thus, in our algebraic setting, we will specify a software component by a pair of specifications SP and SP′, written SP⟶^{ι}SP′, where SP specifies the symbols and their properties required by the component, SP′ specifies the symbols and the properties provided by the component, together with a signature morphism ι: Sig[SP] → Sig[SP′] relating the parameter signature to the result signature. Indeed we require ι to be a specification morphism ι: SP → SP′, i.e., for all M′ ∈ [[SP′]], M′ _{ι} ∈ [[SP]]. This amounts to demanding that the result specification SP′ includes the properties of the parameter required by the parameter specification SP. The fact that the result actually has those properties is guaranteed by the persistency of the local construction.

The following definition states when a local construction F, determined by a software component ΔP, is a correct realization of a given component specification. (We refer to this as literal correctness by contrast with the observational correctness of Def. 6.9 below.)

Definition 3.2 (Literal correctness). A local construction F along ι: Sig[SP] → Sig[SP′] is literally correct w.r.t. SP and SP′ if for all models M ∈ [[SP]], M ∈ dom(F) and F (M) ∈ [[SP′]]. We write [[SP⟶^{ι}SP′]] for the class of all local constructions along ι that are literally correct w.r.t. SP and SP′.

Hence to realize the component specification SP⟶^{ι}SP′, we should provide a software component ΔP that extends any realization P of SP to a realization P′ = ΔP (P) of SP′. The basic semantic property required is that for all programs P such that [[P]] ∈ [[SP]], ΔP (P) is a program that extends P and realizes SP′ (semantically: [[ΔP (P)]] _{ι} = [[P]] and [[ΔP (P)]] ∈ [[SP′]]). This amounts to requiring that the partial function F ∈ Mod(Σ⟶^{ι}Σ′) determined by ΔP preserves its argument whenever it is defined, is defined on (at least) all models in [[SP]],^{5} and yields a result in [[SP′]] when applied to a model in [[SP]].

There is a crucial difference here between monolithic self-contained programs and software components: while monolithic programs are modelled as Casl models, software components are modelled as (possibly partial) functions mapping Casl models of the parameter specification SP to Casl models of the result specification SP′.

The next important idea is that when assembling components, in general a given component will not be applied to a sub-system providing exactly what is required by the component; it will be applied to a sub-system providing at least, and in general more than what is required.

4 Composition of derived signature morphisms can be defined in the evident fashion, and equality of

two derived signature morphisms is understood here semantically. 5 Intuitively, ΔP (P) is “statically” well-formed as soon as P has the right signature, but needs to be

defined only for arguments that realize SP.

Technically, this means that we need to look at constructions that map Σ-models to Σ′-models, but applied to parts cut out of “larger” Σ_{G}-models, where this “cutting out” is given as the reduct with respect to a signature morphism γ: Σ → Σ_{G} that fits the local argument signature into its global context.

Throughout the rest of the paper, we will repeatedly refer to the signatures and morphisms in the following pushout diagram:

[figure: Σ; Σ_{G}; Σ′; Σ′_{G}; γ; ι; ι′; γ′]

where the local construction is along the bottom of the diagram, “cutting out” its argument from a larger model uses the signature morphism on the left, and the resulting global construction is along the top.

Definition 3.3 (Admissibility and global construction). Given a local construction F along a signature morphism ι: Σ → Σ′, a morphism γ: Σ → Σ_{G} fitting Σ into a “global” signature Σ_{G} is admissible if the pushout of ι and γ above ensures amalgamability. Then, for any Σ_{G}-model G ∈ |Mod(Σ_{G})|, we define the global result F_{G}(G) of applying F to G by reference to the pushout diagram above, using the amalgamation property: if G _{γ} ∈ dom(F) then F_{G}(G) = G ⊕ F (G _{γ}); otherwise F_{G}(G) is undefined.

This determines a global construction F_{G}: |Mod(Σ_{G})| ⇀ |Mod(Σ′_{G})|, which is persistent along ι′: Σ_{G} → Σ′_{G}.

This way of “lifting” a persistent function to a larger context via a “fitting morphism” using signature pushout and amalgamation is well established in the algebraic specification tradition, going back at least to “parametrized specifications” with free functor semantics, see (Ehrig and Mahr 1985). The extra requirement here is that only admissible fitting morphisms are permitted, turning amalgamability into a (static) requirement for correct application of a local construction in a given context, to be discharged using the machinery of (Schröder et al. 2001; Klin et al. 2001; Schröder et al. 2005).

Then an obvious issue is whether a software component that realizes a component specification SP⟶^{ι}SP′, when combined with a sub-system that realizes a specification SP_{G}, actually provides a system that realizes a given specification SP′_{G}. The corresponding correctness condition is provided by the following theorem.

Theorem 3.4. Given a local construction F ∈ [[SP⟶^{ι}SP′]], a specification SP_{G} with admissible fitting morphism γ: Sig[SP] → Sig[SP_{G}], and a specification SP′_{G} with Sig[SP′_{G}] = Σ′_{G}, the induced global construction F_{G} along ι′: Σ_{G} → Σ′_{G} is literally correct w.r.t. SP_{G} and SP′_{G}, i.e., F_{G} ∈ [[SP_{G}⟶^{ι′}SP′_{G}]], provided that:

— [[SP_{G}]] ⊆ [[SP with γ]], and

— [[(SP′ with γ′) and (SP_{G} with ι′)]] ⊆ [[SP′_{G}]].

Proof. Let G ∈ [[SP_{G}]]. Then G _{γ} ∈ [[SP]], and so G _{γ} ∈ dom(F) and F (G _{γ}) ∈ [[SP′]]. Consequently F_{G}(G) ∈ [[SP′ with γ′]] ∩ [[SP_{G} with ι′]].

Informally, this captures directly a “bottom-up” process of building component-based systems, whereby we start with SP_{G}, a specification of a “global” assembly of components built so far, find a local construction (a component) F ∈ [[SP⟶^{ι}SP′]] with a fitting morphism γ that satisfies the first condition, and define SP′_{G} such that the second condition is satisfied (e.g. by simply taking SP′_{G} = (SP′ with γ′) and (SP_{G} with ι′)), thus obtaining a specification of the global assembly of components with the new component built using F added. When proceeding “top-down”, we start with the global requirements specification SP′_{G}. To use a local construction (a component) F ∈ [[SP⟶^{ι}SP′]], we have to decide which part of the requirements it is going to implement by providing a signature morphism γ′: Sig[SP′] → Sig[SP′_{G}], then construct the “pushout complement” γ: Sig[SP] → Σ_{G}, ι′: Σ_{G} → Sig[SP′_{G}] for ι and γ′, and finally devise a specification SP_{G} with Sig[SP_{G}] = Σ_{G} such that both conditions are satisfied. Then SP_{G} is the requirements specification for the components that remain to be implemented.

4. Architectural Specifications

Using local constructions for global implementations of specifications, we have moved only one step away from a monolithic global view of specifications and constructions used to implement them. The notion of architectural specification (Bidoit, Sannella and Tarlecki 2002a) as introduced for Casl takes us much further. An architectural specification prescribes a decomposition of the task of implementing a requirements specification into a number of subtasks to implement specifications of “modular components” (called units) of the system under development. The units may be parametrized, and then we can identify them with local constructions; non-parametrized units are just models. Another essential part of an architectural specification is a prescription of how the units, once developed, are to be put together using a few simple operators. One of these is application of a parametrized unit which corresponds exactly to the lifting of a local construction to a larger context studied above. Thus, an architectural specification may be thought of as a definition of a complex construction to be used in a top-down development process to implement a requirements specification by a number of specifications (of non-parametrized units), where the construction uses a number of specified local constructions that are to be developed as well.

For the sake of readability, we will discuss here a simplified version of Casl architectural specifications, with a limited (but representative) number of constructs, shaped after a version used in (Schröder et al. 2001; Schröder et al. 2005); a generalization to full architectural specifications (including unit renaming, units with multiple parameters, local unit definitions, etc.) would be tedious but rather straightforward, except perhaps for the “unguarded import” mechanism, see (Hoffman 2001). Our version of architectural specifications is defined as follows. Architectural specifications: ASP ::= arch spec UDD^{+} result T ;

UDD ::= Dcl | Dfn

An architectural specification consists of a (non-empty) list of unit declarations or definitions followed by a unit result term.

Unit declarations: Dcl ::= U : SP | U : SP_{1}⟶^{ι}SP_{2} A unit declaration introduces a unit name with its type, which is either a specification or a specification of a parametrized unit, determined by a specification of its parameter and its result that extends the parameter via a signature morphism ι.

Unit definitions: Dfn ::= U = T A unit definition introduces a (non-parametrized) unit and gives its value by a unit term.

Unit terms: T ::= U | reduce T by σ | U [T fit γ] | T_{1} and T_{2} A unit term is either a (non-parametrized) unit name, or a unit restricted w.r.t. a signature morphism, or a unit application with an argument that fits via a signature morphism γ, or an amalgamation of units. Following the semantics of full Casl (Baumeister et al. 2004), see also (Schröder et al.

2001; Schröder et al. 2005), we give the semantics of this Casl fragment in two stages: first we give its extended static semantics^{6} and then its literal model semantics. (We refer to this as the literal model semantics by contrast with the observational model semantics of Sect. 7 below.)

For the extended static semantics we need a concept of static context, which carries signatures for the units declared or defined within an architectural specification, together with information on their mutual dependencies. Analogously, for the model semantics we need a concept of environment, which carries the semantics of the units named in the corresponding static context.

When discussing application of local constructions to global models in Sect. 3, we viewed the global context as a single monolithic model over a single “global” signature. Unfortunately, in the context of architectural specifications in Casl this view cannot be maintained. The technical reason is that Casl does not ensure amalgamation over arbitrary colimits of signature diagrams, as pointed out in Sect. 2. Indeed, if amalgamability were ensured for arbitrary colimits of signature diagrams, we could always represent the global context of all the (non-parametrized) units declared or defined so far by a monolithic global model over a single global signature, and many of the technicalities below become rather simpler, see (Bidoit, Sannella and Tarlecki 2002b; Tarlecki 2003). As things are, for architectural specifications in Casl, static information about (nonparametrized) units declared or defined in an architectural specification will be stored in signature diagrams, with nodes labeled by unit signatures and edges labeled by signature morphisms that capture dependencies between units.

More formally, we view a signature diagram as a graph morphism from its shape I to the category of Casl signatures, D : I → Sig. We write |D| for the set of nodes of I, and m: i → j in D for an edge m with source i and target j in I. The extension of diagrams is understood as usual. Two diagrams D_{1}, D_{2} disjointly extend D if both D_{1} and D_{2} extend D and the intersection of their shapes is the shape of D. If this is the case then the union D_{1} ∪ D_{2} is well-defined. As usual, disjointness of diagram extensions may be ensured by choosing the new nodes and edges appropriately.

6 In (Baumeister et al. 2004), a distinction is made between static semantics of architectural specifications, which ignores dependencies between terms and hence does not contribute to the analysis of amalgamability, and extended static semantics.

For any diagram D : I → Sig, a family M = ⟨M_{i}⟩_{i∈|D|} of models is called D-coherent if for each i ∈ |D|, M_{i} ∈ |Mod(D(i))|, and for each m: i → j in I, M_{i} = M_{j} _{D(m)}; this is extended to |D|-indexed families of model morphisms in the obvious way. Given a D-coherent family M = ⟨M_{i}⟩_{i∈|D|}, we write M_{i} for M_{i}, i ∈ |D|. We let Mod(D) be the category with D-coherent model families as objects and D-coherent families of model morphisms as morphisms (with the obvious component-wise composition).

D ensures amalgamability for D′, where D′ extends D, if any D-coherent model family can be uniquely extended to a D′-coherent model family. It is easy to see that Def. 2.1 is in fact a special case of this notion.^{7}

An extended static context C_{st} = (P_{st}, B_{st}, D), in which Casl phrases are elaborated, consists of a static context for parametrized units P_{st} mapping parametrized unit names to signature morphisms (from the parameter to the result signature), a global context diagram D, and a static context for non-parametrized units B_{st} mapping non-parametrized unit names to nodes in D. From any such extended static context we can extract a static context ctx(C_{st}) = (P_{st}, B_{st}) by preserving the static context P_{st} for parametrized units and building a direct static context B_{st} for non-parametrized units that extracts their signatures from B_{st} and D (i.e., B_{st}(U ) = D_{B_{st} (U )}). C_{st}^{∅} stands for the “empty” extended static context that consists of the empty parametrized and non-parametrized unit contexts, and of the empty context diagram. Extension (or inclusion) of extended static contexts, written C_{st} ⊆ C′_{st}, is defined component-wise, as expected. We refer to unit names in dom(P_{st}) as parametrized unit names in C_{st}, and to those in dom(B_{st}) as non-parameterized unit names in C_{st}.

Figure 1 gives rules to derive semantic judgments of the following forms:

— ⊢ ASP ⊳ ⊳ ((P_{st}, B_{st}), Σ): the architectural specification ASP yields a static context describing the units declared or defined in ASP, and the signature of the result unit;

— ⊢ UDD^{+} ⊳ ⊳ C_{st}: the sequence UDD^{+} of unit declarations and definitions yields an extended static context C_{st};

— C_{st} ⊢ UDD ⊳ ⊳ C′_{st}: the unit declaration or definition UDD in the extended static context C_{st} yields a new extended static context C′_{st} which extends C_{st};

— (P_{st}, B_{st}, D) ⊢ T ⊳ ⊳ (i, D′): the unit term T in the extended static context (P_{st}, B_{st}, D) yields a new context diagram D′ which extends D and a node i in D′ that carries the signature of the unit term T .

To follow the rules for unit application and amalgamation, it may be helpful to look at Fig. 2, where the corresponding global context diagrams are sketched.

It is worth noting that in the rule for parametrized unit application, the requirement that D′ ensures amalgamability for D′′ is weaker than requiring that the pushout used in this rule ensures amalgamability: even if it does not, the global context in which the

7 In spite of Lemma 2.2 and its obvious generalization to colimits of arbitrary signature diagrams, we do not know whether in the framework of Casl it is always the case that if D ensures amalgamability for D′ then also the similar property holds for D-coherent families of model morphisms; we conjecture that this is the case. However, in this paper we need only a few special cases of this, where D′ arises from D essentially by adding a surjective cone, and so a proof similar to that for Lemma 2.2 goes through; the same is true for a similar generalisation of Lemma 5.6 below.

Observational Interpretation of Casl Specifications 15

\frac{⊢ UDD^{+} ⊳ ⊳ C_{st} C_{st} ⊢ T ⊳ ⊳ (i, D)}{⊢ arch spec UDD^{+} result T ⊳ ⊳ (ctx(C_{st}), D(i))}

\frac{C_{st}^{∅} ⊢ UDD_{1} ⊳ ⊳ (C_{st})_{1} ⋯ (C_{st})_{n−1} ⊢ UDD_{n} ⊳ ⊳ (C_{st})_{n}}{⊢ UDD_{1} … UDD_{n} ⊳ ⊳ (C_{st})_{n}}

\frac{U ∉ (dom(P_{st}) ∪ dom(B_{st})) D′ extends D by a new node i with D′(i) = Sig(SP)}{(P_{st}, B_{st}, D) ⊢ U : SP ⊳ ⊳ (P_{st}, B_{st} + \{U ↦ i\}, D′)}

\frac{ι : Sig(SP_{1}) → Sig(SP_{2}) U ∉ (dom(P_{st}) ∪ dom(B_{st}))}{(P_{st}, B_{st}, D) ⊢ U : SP_{1}⟶^{ι}SP_{2} ⊳ ⊳ (P_{st} + \{U ↦ ι\}, B_{st}, D)}

\frac{(P_{st}, B_{st}, D) ⊢ T ⊳ ⊳ (i, D′) U ∉ (dom(P_{st}) ∪ dom(B_{st}))}{(P_{st}, B_{st}, D) ⊢ U = T ⊳ ⊳ (P_{st}, B_{st} + \{U ↦ i\}, D′)}

\frac{U ∈ dom(B_{st})}{(P_{st}, B_{st}, D) ⊢ U ⊳ ⊳ (B_{st}(U ), D)}

C_{st} ⊢ T ⊳ ⊳ (i, D) σ: Σ → D(i)

D′ extends D by a new node j and a new edge m: j → i with D′(m) = σ C_{st} ⊢ reduce T by σ ⊳ ⊳ (j, D′)

P_{st}(U ) = ι: Σ → Σ′  C_{st} ⊢ T ⊳ ⊳ (i, D)  γ: Σ → D(i)
(ι′, γ′) is a pushout of (γ, ι)

D′ extends D by new nodes j, k and edges m: j → i, n: j → k

with D′(m) = γ, D′(n) = ι

D′′ extends D′ by a new node l and edges r: i → l, s: k → l

with D′′(r) = ι′, D′′(s) = γ′

D′ ensures amalgamability for D′′ C_{st} ⊢ U [T fit γ] ⊳ ⊳ (l, D′′)

(P_{st}, B_{st}, D) ⊢ T_{1} ⊳ ⊳ (i_{1}, D_{1}) (P_{st}, B_{st}, D) ⊢ T_{2} ⊳ ⊳ (i_{2}, D_{2})

D_{1} and D_{2} are disjoint extensions of D

D′ extends D_{1} ∪ D_{2} by a new node j and edges m_{1}: i_{1} → j, m_{2}: i_{2} → j with

D′(j) = D_{1}(i_{1}) ∪ D_{2}(i_{2}), D′(m_{1}): D_{1}(i_{1}) ↪ D′(j), D′(m_{2}): D_{2}(i_{2}) ↪ D′(j)

D_{1} ∪ D_{2} ensures amalgamability for D′

(P_{st}, B_{st}, D) ⊢ T_{1} and T_{2} ⊳ ⊳ (j, D′)

Fig. 1. Extended static semantics

[figure: D; D(i); D′(j) = Σ; D′(k) = Σ′; D′′(l); D′(m) = γ; D′′(r) = ι′; D′(n) = ι; D′′(s) = γ′; D; D_{1}; D_{1}(i_{1}); D_{2}; D_{2}(i_{2}); D′(j); D′(m_{1}); D′(m_{2})]

Fig. 2. Unit application and amalgamation diagrams

application is carried out may impose additional constraints on the models involved that ensure amalgamability.

Note also that the rule for unit amalgamation does not require that the amalgamated units have common signatures: the resulting unit will be built over the union of the two signatures, provided that this union is defined^{8} and that the two units built can be uniquely amalgamated to yield a unit over this union signature. This is ensured by the final condition in the rule, which requires that the dependencies between units captured in the diagram D_{1} ∪ D_{2} ensure amalgamability of the two models involved. This requires in particular that these models share the interpretation of the symbols in the intersection of their signatures.

In the model semantics we work with contexts C that are classes of unit environments E. Unit environments map unit names to either local constructions (for parametrized units) or to individual models (for non-parametrized units). Unit evaluators UEv map unit environments to models.

Given an extended static context C_{st} = (P_{st}, B_{st}, D), a unit environment E fits C_{st} if

— for each U ∈ dom(P_{st}), E(U ) is a local construction along P_{st}(U ), and

— there is a D-coherent family of models M ∈ |Mod(D)| such that for each U ∈ dom(B_{st}), E(U ) = M_{B_{st} (U )}; we say then that M witnesses E in C_{st}.

We write ucx(C_{st}) for the class of all unit environments that fit C_{st}. Note that if C_{st} ⊆ C′_{st} then ucx(C′_{st}) ⊆ ucx(C_{st}).

8 The union is defined in the obvious, component-wise manner, with the subsort preorder given as the transitive closure of the two preorders in the component signatures — however, this may fail to yield a Casl signature due to overloading of operation and predicate names that may arise, which we have disallowed here. The union may also fail to be defined with Casl’s treatment of overloading, albeit for more subtle reasons.

Two unit environments E_{1}, E_{2} ∈ ucx(C_{st}) coincide in C_{st}, written E_{1} =_{C_{st}} E_{2}, if for all (parametrized and non-parametrized) unit names U in C_{st}, E_{1}(U ) = E_{2}(U ).

Proposition 4.1. If E_{1} =_{C_{st}} E_{2} then any family that witnesses E_{1} in C_{st}, witnesses E_{2} in C_{st} as well.

A context C ⊆ ucx(C_{st}) is closed in C_{st} if for all unit environments E_{1} ∈ C and E_{2} ∈ ucx(C_{st}), E_{1} =_{C_{st}} E_{2} implies E_{2} ∈ C.

C^{∅} = ucx(C_{st}^{∅}) is the context which constrains no unit name. Given a context C, a unit name U and a class of units V, we write C×{U ↦ V} for {E +{U ↦ V } | E ∈ C, V ∈ V}, where E + {U ↦ V } maps U to V and otherwise behaves like E.

Figure 3 gives rules to derive semantic judgments of the following forms:

— ⊢ ASP ⇒ (C, UEv): the architectural specification ASP yields a context C with environments providing interpretations for the units declared and defined in ASP, and a unit evaluator that for each such environment determines the result unit;

— ⊢ UDD^{+} ⇒ C: the sequence UDD^{+} of unit declarations and definitions yields a context C;

— C ⊢ UDD ⇒ C′: the unit declaration or definition UDD in the context C yields a new context C′;

— C ⊢ T ⇒ UEv: the unit term T in the context C yields a unit evaluator UEv that when given an environment (in C) yields the unit resulting from the evaluation of T in this environment.

The rules rely on a successful run of the extended static semantics; this allows us to use the static concepts and notations introduced there. The crossed-out premises in the rules are crucial properties that are guaranteed to hold for phrases for which the extended static semantics yields a result, as a consequence of the following theorem.

Theorem 4.2. The following invariants link the extended static semantics and model semantics: 1 If ⊢ ASP ⊳ ⊳ ((P_{st}, B_{st}), Σ) and ⊢ ASP ⇒ (C, UEv) then there is an extended static

context C_{st} such that ctx(C_{st}) = (P_{st}, B_{st}) and C ⊆ ucx(C_{st}), C is closed in C_{st}, and for each E ∈ C, E ∈ dom(UEv) and UEv(E) ∈ |Mod(Σ)|. Moreover, for E_{1}, E_{2} ∈ C, if E_{1} =_{C_{st}} E_{2} then UEv(E_{1}) = UEv(E_{2}).

2 If ⊢ UDD^{+} ⊳ ⊳ C_{st} and ⊢ UDD^{+} ⇒ C then C ⊆ ucx(C_{st}) and C is closed in C_{st}. 3 If C_{st} ⊢ UDD ⊳ ⊳ C′_{st} and C ⊢ UDD ⇒ C′, where C ⊆ ucx(C_{st}) and C is closed in C_{st},

then C′ ⊆ ucx(C′_{st}), C′ ⊆ C, C′ is closed in C′_{st} and for each unit environment E ∈ C and model family M that witnesses E in C_{st}, there is E′ ∈ C′ such that E =_{C_{st}} E′ and an extension of M witnesses E′ in C′_{st}.

4 If C_{st} ⊢ T ⊳ ⊳ (i, D′) and C ⊢ T ⇒ UEv with C ⊆ ucx(C_{st}), then for each unit environment E ∈ C and model family M that witnesses E in C_{st}, there is an extension of M to a D′-coherent model family M′ ∈ |Mod(D′)| such that M′_{i} = UEv(E). Moreover, for E_{1}, E_{2} ∈ C, if E_{1} =_{C_{st}} E_{2} then UEv(E_{1}) = UEv(E_{2}).

Proof. Item 4 is proved by induction on the structure of the unit term. The fact that the value of the unit evaluator on an environment does not change when it does not depend

\frac{⊢ UDD^{+} ⇒ C C ⊢ T ⇒ UEv}{⊢ arch spec UDD^{+} result T ⇒ (C, UEv)}

\frac{\begin{matrix}C^{∅} ⊢ UDD_{1} ⇒ C_{1} \\ ⋯ \\ C_{n−1} ⊢ UDD_{n} ⇒ C_{n} \end{matrix}}{⊢ UDD_{1} … UDD_{n} ⇒ C_{n}}

\overline{C ⊢ U : SP ⇒ C × \{U ↦ [[SP]]\}}

C ⊢ U : SP_{1}⟶^{ι}SP_{2} ⇒ C × {U ↦ [[SP_{1}⟶^{ι}SP_{2}]]}

\frac{C ⊢ T ⇒ UEv}{C ⊢ U = T ⇒ \{E + \{U ↦ UEv(E)\} | E ∈ C\}}

\overline{C ⊢ U ⇒ λE ∈ C · E(U )}

\frac{C ⊢ T ⇒ UEv}{C ⊢ reduce T by σ ⇒ λE ∈ C · UEv(E) _{σ}}

\frac{C ⊢ T ⇒ UEv for each E ∈ C, UEv(E) _{γ} ∈ dom(E(U )) for each E ∈ C, UEv(E) ⊕ E(U )(UEv(E) _{γ}) is well-defined}{C ⊢ U [T fit γ] ⇒ λE ∈ C · UEv(E) ⊕ E(U )(UEv(E) _{γ})}

\frac{C ⊢ T_{1} ⇒ UEv_{1} C ⊢ T_{2} ⇒ UEv_{2} for each E ∈ C, there is a unique M ∈ |Mod(Σ)| such that M _{ι_{1}} = UEv_{1}(E), M _{ι_{2}} = UEv_{2}(E) UEv = \{E ↦ M | E ∈ C, M _{ι_{1}} = UEv_{1}(E), M _{ι_{2}} = UEv_{2}(E)\}}{C ⊢ T_{1} and T_{2} ⇒ UEv}

Fig. 3. Literal model semantics

on the values in the environment not mentioned in the static context (for E_{1}, E_{2} ∈ C, if E_{1} =_{C_{st}} E_{2} then UEv(E_{1}) = UEv(E_{2})) follows in each case easily, using the inductive hypothesis.

The case of unit name is trivial, and the case of unit reduct is very easy.

Consider the case of unit application, when the unit term is of the form U [T fit γ]. Adjusting the notation slightly to fit the corresponding rules (for unit application) in Figs. 1 and 3 (we will implicitly rely below on the notation used in these rules), assume that C ⊆ ucx(C_{st}), C_{st} ⊢ U [T fit γ] ⊳ ⊳ (l, D′′) and C ⊢ U [T fit γ] ⇒ UEv′, where UEv′(E) = UEv(E) ⊕ E(U )(UEv(E) _{γ}) for E ∈ C. Consequently, all the premises of the corresponding rules (for unit application) in Figs. 1 and 3 must hold. Let E ∈ C and M be a model family that witnesses E in C_{st}. By the inductive hypothesis, there is an extension M^{T} ∈ |Mod(D)| of M such that M_{i}^{T} = UEv(E). Let M′ extend M^{T} by putting M′_{j} = UEv(E) _{γ} and M′_{k} = E(U )(UEv(E) _{γ}) (since UEv(E) _{γ} ∈ dom(E(U )), the latter is well-defined). Then M′ ∈ |Mod(D′)|. Since D′ ensures amalgamability for D′′, M′ uniquely extends to M′′ ∈ |Mod(D′′)|, yielding M′′_{l} _{ι′} = M′_{i} and M′′_{l} _{γ′} = M′_{k}, that is, M′′_{l} = UEv(E) ⊕ E(U )(UEv(E) _{γ}) — which completes the proof for this case.

For the case of unit amalgamation, when the unit term is of the form T_{1} and T_{2}, assume C ⊆ ucx(C_{st}), C_{st} ⊢ T_{1} and T_{2} ⊳ ⊳ (j, D′) and C ⊢ T_{1} and T_{2} ⇒ UEv, where C_{st} = (P_{st}, B_{st}, D). Consequently, all the premises of the corresponding rules (for unit amalgamation) in Figs. 1 and 3 must hold; we refer below to the notations used in the rules. Let E ∈ C and M be a model family that witnesses E in C_{st}. By the inductive hypothesis, there are extensions M^{1} ∈ |Mod(D_{1})| and M^{2} ∈ |Mod(D_{2})| of M such that M_{i_{1}}^{1} = UEv_{1}(E) and M_{i_{2}}^{2} = UEv_{2}(E). Since D_{1} and D_{2} are disjoint extensions of D, M^{1} ∪M^{2} is a (D_{1} ∪D_{2})-coherent family of models. Now, since D_{1} ∪D_{2} ensures amalgamability for D′, M^{1} ∪M^{2} extends uniquely to a D′-coherent family M′ ∈ |Mod(D′)|, necessarily with M′_{j} _{D′(m_{1})} = M_{i_{1}}^{1} and M′_{j} _{D′(m_{2})} = M_{i_{2}}^{2}, that is, M′_{j} = UEv(E) — which completes the proof of item 4.

Item 3 follows by inspection of the rules; the cases of unit declarations are easy. The case of unit definitions relies on item 4 as follows. Assume that C ⊆ ucx(C_{st}) and C is closed in C_{st}, C_{st} = (P_{st}, B_{st}, D). To derive C_{st} ⊢ UDD ⊳ ⊳ C′_{st} and C ⊢ UDD ⇒ C′, where UDD is of the form U = T , we must have (P_{st}, B_{st}, D) ⊢ T ⊳ ⊳ (i, D′), U ∉ (dom(P_{st}) ∪ dom(B_{st})), and C ⊢ T ⇒ UEv, with C′_{st} = (P_{st}, B_{st} + {U ↦ i}, D′) and C′ = {E + {U ↦ UEv(E)} | E ∈ C}. Now, for each E ∈ C and model family M ∈ |Mod(D)| that witnesses E in C_{st}, by item 4 there exists an extension M′ ∈ |Mod(D′)| of M with M′_{i} = UEv(E). M′ witnesses E + {U ↦ UEv(E)} in C′_{st}. Consequently, we have C′ ⊆ ucx(C′_{st}). Moreover, since C is closed in C_{st} and U ∉ (dom(P_{st}) ∪ dom(B_{st})), (E + {U ↦ UEv(E)) ∈ C, which shows C′ ⊆ C. Finally, C′ is closed in C′_{st} since C is closed in C_{st}.

Item 2 follows from item 3 by an obvious induction on the length of the sequence of unit declarations and definitions.

Finally, item 1 follows from items 2 and 4 by inspection of the rules. Namely, to derive the assumptions for ASP of the form arch spec UDD^{+} result T , we must have ⊢ UDD^{+} ⊳ ⊳ C_{st} and ⊢ UDD^{+} ⇒ C, as well as C_{st} ⊢ T ⊳ ⊳ (i, D) and C ⊢ T ⇒ UEv, with (P_{st}, B_{st}) = ctx(C_{st}) and Σ = D(i). The thesis now follows directly from items 2 and 4.

The invariants in Thm. 4.2 ensure that the crossed out premises of the unit amalgamation rule and of the parametrized unit application rule in the literal model semantics follow from the other premises of the rule and the premises of the corresponding rules of the extended static semantics.

5. Observational Equivalence for Casl Models

So far, we have followed the usual interpretation for basic specifications given as sets of axioms over some signature, which is to require models of such a basic specification to satisfy all its axioms. This is what is captured by the notion of literal correctness (Def. 3.2) and the literal model semantics of Fig. 3. However, in many practical examples this turns out to be overly restrictive. The point is that only a subset of the sorts in the signature of a specification are typically intended to be directly observable while the others are treated as internal, with properties of their elements made visible only via observations: terms producing a result of an observable sort, and predicates. Often there are models that do not satisfy the axioms “literally” but in which all observations nevertheless deliver the required results. This calls for a relaxation of the interpretation of specifications, as advocated in numerous “observational” or “behavioural” approaches, going back at least to (Giarratana, Gimona and Montanari 1976; Reichel 1981). Two general approaches are possible:

— introduce an “internal” observational indistinguishability relation between elements in the carrier of each model, and re-interpret equality in the axioms as indistinguishability; or

— introduce an “external” observational equivalence relation on models over each signature, and re-interpret specifications by closing their class of models under such equivalence.

It turns out that under some acceptable technical conditions, these two approaches are closely related and coincide for most basic specifications (Bidoit, Hennicker and Wirsing 1995; Bidoit and Tarlecki 1996). We follow the second approach here.

From now on we will assume that the set of observable sorts is empty and so predicates are the only observations. In view of this decision, there is no need to parametrize the definitions below by a chosen set of observable sorts. This departs from standard approaches to observational equivalence in the usual algebraic frameworks, where choosing a non-empty set of observable sorts is crucial to have any observations at all. Moreover, it is appropriate for this set to vary in the process of modular development, where some sorts must be locally considered as observable (e.g. the parameter sorts in specifications of local constructions). The former is taken care of by assuming that appropriate predicates are introduced into the specifications considered. For instance, to make a generated sort observable, it is enough to introduce the “equality predicate” on this sort into the specification.^{9} The latter will be achieved in a technically different way here, see Def. 6.9 below and the subsequent comment.

We should also note here that for each Casl signature Σ and sort s in Σ we have s ≤ s, and so we also have a predicate in^{s≤s}: s, which holds for all its arguments in any Casl model. This means that given a Σ-term t of sort s, in^{s≤s}(t) holds if and only if t has a defined value. Consequently, observing predicates in Casl models covers observing definedness of terms.

Given a Casl signature Σ, an observation is an atomic predicate formula ϕ of the form p(t_{1}, …, t_{n}), where p: s_{1} × ⋯ × s_{n} is a predicate symbol in Σ^{#} and for i = 1, …, n, t_{i} is a

9 Some free datatype definitions in Casl ensure that the new sort is observable even though no equality predicate is explicitly introduced. This is the case when there is a subsort for each alternative and selectors for each non-constant constructor. Then enough observations are available to distinguish between any two data values, provided that the other argument sorts for the constructors are observable (come with enough observations to distinguish between any data of these sorts).

Σ^{#}-term of sort s_{i}. The observation p(t_{1}, …, t_{n}) is closed if all the terms t_{i}, i = 1, …, n, are closed (contain no variables). Given a sort s in Σ, the observation p(t_{1}, …, t_{n}) is for sort s if it contains a unique variable z: s of sort s (and no other variables at all). We will often write then ϕ(z) to indicate the variable explicitly, and for a Σ^{#}-term t of sort s, we write ϕ(t) for the result of substituting t for z in ϕ.

Definition 5.1 (Observational equivalence). Given a Casl signature Σ, two Σmodels M, N ∈ |Mod(Σ)| are observationally equivalent, written M ≡ N, if for all closed observations ϕ,

M ⊧ ϕ ⟺ N ⊧ ϕ

It is trivial to see that observational equivalence is indeed an equivalence on Casl models over any signature Σ.

In the following we will work with a technically different but equivalent definition of observational equivalence, where the equivalence of two models is “witnessed” by a relation between them; this has been worked out in detail (for partial algebras without predicates) in (Schoett 1987), cf. “simulations” in (Milner 1971) and “weak homomorphisms” in (Ginzburg 1968).

Definition 5.2 (Correspondence). Consider a signature Σ. A correspondence between two Σ-models M, N ∈ |Mod(Σ)|, written ρ: M ▷◁ N, is a relation ρ ⊆ |M| × |N| that

— is closed under the operations: for f: s_{1} × … × s_{n} → s in Σ^{#}, a_{1} ∈ |M|_{s_{1}}, …, a_{n} ∈ |M|_{s_{n}} and b_{1} ∈ |N|_{s_{1}}, …, b_{n} ∈ |N|_{s_{n}}, if (a_{1}, b_{1}) ∈ ρ_{s_{1}}, …, (a_{n}, b_{n}) ∈ ρ_{s_{n}} then f_{M}(a_{1}, …, a_{n}) is defined iff f_{M}(b_{1}, …, b_{n}) is defined, and if so then (f_{M}(a_{1}, …, a_{n}), f_{N}(b_{1}, …, b_{n})) ∈ ρ_{s}; and

— preserves and reflects the predicates: for p: s_{1} × … × s_{n} in Σ^{#}, a_{1} ∈ |M|_{s_{1}}, …, a_{n} ∈ |M|_{s_{n}} and b_{1} ∈ |N|_{s_{1}}, …, b_{n} ∈ |N|_{s_{n}}, if (a_{1}, b_{1}) ∈ ρ_{s_{1}}, …, (a_{n}, b_{n}) ∈ ρ_{s_{n}} then p_{M}(a_{1}, …, a_{n}) ⟺ p_{N}(b_{1}, …, b_{n}).

In the rest of the paper we will rely on the following equivalence without further mention:

Theorem 5.3. Given a Casl signature Σ, Σ-models M, N ∈ |Mod(Σ)| are observationally equivalent if and only if there is a correspondence between them.

Proof. Let M ≡ N. Define a relation ρ ⊆ |M| × |N| to contain, for each sort s in Σ, all and only pairs of the form (t_{M}, t_{N}), for all closed Σ^{#}-terms t of sort s such that the value of t is defined in both M and N. To check that ρ is a correspondence between M and N, consider for i = 1, …, n, a_{i} ∈ |M|_{s_{i}} and b_{i} ∈ |N|_{s_{i}} such that (a_{i}, b_{i}) ∈ ρ_{s_{i}}, so that a_{i} = (t_{i})_{M} and b_{i} = (t_{i})_{N} for some Σ^{#}-term t_{i} of sort s_{i}. Consider now f: s_{1} × … × s_{n} → s in Σ^{#}. Since M ≡ N, M ⊧ in^{s≤s}(f(t_{1}, …, t_{n})) iff N ⊧ in^{s≤s}(f(t_{1}, …, t_{n})); so, f_{M}(a_{1}, …, a_{n}) is defined iff f_{M}(b_{1}, …, b_{n}) is defined, and if so then by definition (f_{M}(a_{1}, …, a_{n}), f_{N}(b_{1}, …, b_{n})) ∈ ρ_{s} (since (f(t_{1}, …, t_{n}))_{M} = f_{M}(a_{1}, …, a_{n}) and (f(t_{1}, …, t_{n}))_{N} = f_{N}(b_{1}, …, b_{n})). Similarly, for p: s_{1}×…×s_{n} in Σ^{#}, M ⊧ p(t_{1}, …, t_{n}) iff N ⊧ p(t_{1}, …, t_{n}), which shows the equivalence of p_{M}(a_{1}, …, a_{n}) and p_{N}(b_{1}, …, b_{n}), and completes the proof of ρ: M ▷◁ N.

Consider now a correspondence ρ: M ▷◁ N. Using the correspondence properties, by simple induction on the term structure, for any closed Σ^{#}-term t, one can prove that t_{M} is defined iff t_{N} is defined, and if so then (t_{M}, t_{N}) ∈ ρ. Now, given any closed observation p(t_{1}, …, t_{n}), by symmetry it is enough to prove that if M ⊧ p(t_{1}, …, t_{n}) then also N ⊧ p(t_{1}, …, t_{n}). Suppose M ⊧ p(t_{1}, …, t_{n}). Then for i = 1, …, n, (t_{i})_{M} is defined, and so (t_{i})_{N} is defined and ((t_{i})_{M}, (t_{i})_{N}) ∈ ρ. Moreover, p_{M}((t_{1})_{M}, …, (t_{n})_{M}) holds, so by the correspondence property, p_{N}((t_{1})_{N}, …, (t_{n})_{N}) holds as well. Thus N ⊧ p(t_{1}, …, t_{n}).

It is easy to check that isomorphisms (and in particular, identities) are correspondences and that the class of correspondences is closed under composition.

Correspondences between Casl models may be replaced by spans of strong homomorphisms. Namely, given a span of strong homomorphisms (h_{M}: K → M, h_{N}: K → N), putting ρ = h_{M}^{−1};h_{N}, i.e. ρ_{s} = {(h_{M}(c), h_{N}(c)) | c ∈ |K|_{s}} for each sort s in Σ, yields a correspondence ρ: M ▷◁ N. In the opposite direction:

Proposition 5.4. For any Casl signature Σ, Σ-models M, N and correspondence ρ: M ▷◁ N, there is a Σ-model K and strong Σ-homomorphisms h_{M}: K → M and h_{N}: K → N such that ρ = h_{M}^{−1};h_{N}.

Proof. To define K, first put |K|_{s} = ρ_{s} ⊆ |M|_{s} × |N|_{s} for each sort s in Σ. The operations in K are then defined component-wise, using the operations in M and N respectively. The predicates in K are defined either using the first components and the predicates in M, or (equivalently) using the second components and the predicates in N. The correspondence properties of ρ ensure that no problems arise, and that the projection functions h_{M}: K → M and h_{N}: K → N are strong Σ-homomorphisms.

This proposition directly implies that the reduct of a correspondence along a signature morphism (defined in the obvious way) is a correspondence. More interestingly, this extends to derived signature morphisms with observable conditions.

Consider a signature Σ. A conditional Σ-term ⟨(ϕ_{i}, t_{i})⟩_{i≥0} is observationally sensible if for all i ≥ 0, ϕ_{i} are observers, that is, Boolean combinations of observations. A derived signature morphism δ: Σ′ → Σ is observationally sensible if it maps Σ′-operations to observationally sensible terms.

Lemma 5.5. Let δ: Σ′ → Σ be an observationally sensible derived signature morphism, and let ρ: M ▷◁ N be a correspondence between Σ-models M, N ∈ |Mod(Σ)|. Then ρ _{δ}: M _{δ} ▷◁ N _{δ} is a correspondence as well.

It follows that reducts with respect to observationally sensible derived signature morphisms extend to strong homomorphisms.

The view of correspondences as spans of homomorphisms also leads to an easy extension to correspondences of the amalgamation property given in Lemma 2.2 for homomorphisms:

Lemma 5.6. Suppose that the following pushout

[figure: Σ; Σ_{1}; Σ′; Σ′_{1}; γ; ι; ι′; γ′]

ensures amalgamability. Then for all correspondences ρ_{1}: M_{1} ▷◁ N_{1} in Mod(Σ_{1}) and ρ′: M′ ▷◁ N′ in Mod(Σ′) such that ρ_{1} _{γ} = ρ′ _{ι} there exists a unique correspondence ρ′_{1}: M′_{1} ▷◁ N′_{1} in Mod(Σ′_{1}) such that ρ′_{1} _{ι′} = ρ_{1} and ρ′_{1} _{γ′} = ρ′, where M′_{1} = M_{1} ⊕ M′ and N′_{1} = N_{1} ⊕ N′.

Proof. A direct proof mimics the proof of Lemma 2.2.

Note though that this does not ensure that amalgamation preserves observational equivalence:

Counterexample 5.7. Let Σ be a signature with a single sort s, and let Σ_{1} extend Σ by a constant a: s. Since there are no predicates in Σ_{1}, all Σ_{1}-models where the constant a is defined are observationally equivalent. Let Σ′ extend Σ by a unary predicate p: s; since there are no closed observations over Σ′, all Σ′-models are observationally equivalent. The pushout signature of the two extensions of Σ is the signature Σ′_{1} with sort s, constant a: s and predicate p: s. Clearly, not all Σ′_{1}-models with defined values of a are observationally equivalent — there is a new closed observation here, namely p(a).

To make the counterexample explicit, let M_{1} be a Σ_{1}-model with a single element, |M_{1}|_{s} = {x}, and a_{M_{1}} = x. Let M′ and M′′ be Σ′-models such that M′ _{Σ} = M′′ _{Σ} = M_{1} _{Σ} and p_{M′}(x) holds while p_{M′′}(x) does not hold. Still, we have M′ ≡ M′′ (and trivially M_{1} ≡ M_{1}). However, (M_{1} ⊕ M′) ≢ (M_{1} ⊕ M′′).

Observational equivalence can also be characterized in terms of internal indistinguishability. Namely, consider a Casl signature Σ and Σ-model M ∈ |Mod(Σ)|. Let ⟨M⟩ be the generated submodel of M having all and only the defined values in M of closed Σ^{#}- terms as elements of the carrier. For any sort s in Σ, given a, a′ ∈ |⟨M⟩|_{s}, we say that a and a′ are observationally indistinguishable in M, written a ≈_{M} a′, if for all observations ϕ for sort s,

M[z ↦ a] ⊧ ϕ ⟺ N[z ↦ a′] ⊧ ϕ

Thus defined observational indistinguishability on M, ≈_{M} ⊆ |⟨M⟩| × |⟨M⟩|, is the largest strong congruence on ⟨M⟩. The observational quotient of M, written M/≈, is the quotient of ⟨M⟩ by ≈_{M}.

Theorem 5.8. Consider a Casl signature Σ. Two Σ-models are observationally equivalent if and only if their observational quotients are isomorphic.

Proof. For all Casl models M, since there is a natural strong homomorphism from ⟨M⟩ to M/≈, which is a correspondence between M and M/≈, we have that M ≡ M/≈. Therefore, given two Casl models M, N ∈ |Mod(Σ)| with isomorphic observational quotients M/≈ and N/≈, we get M ≡ N.

Suppose now M ≡ N. Then for any closed Σ^{#}-term t of a sort s, the value t_{M} of t in M is defined iff the value t_{N} of t in N is defined. Moreover, if this is the case, then for any observation ϕ(z) for sort s:

M[z ↦ t_{M}] ⊧ ϕ(z) ⟺ M ⊧ ϕ(t) ⟺ N ⊧ ϕ(t) ⟺ N[z ↦ t_{N}] ⊧ ϕ(z)

It follows that for any closed Σ^{#}-terms t and t′ of a common sort s, if their values are defined in M (and hence in N as well)

t_{M} ≈_{M} t′_{M} ⟺ t_{N} ≈_{N} t′_{N}

Consequently, a function that for each closed Σ^{#}-term t with defined value in M maps the equivalence class of t_{M} w.r.t. ≈_{M} to the equivalence class of t_{N} w.r.t. ≈_{N} is a welldefined, bijective, strong homomorphism, and hence an isomorphism, between M/≈ and N/≈.

Corollary 5.9. Consider a Casl signature Σ. Σ-models M and N are observationally equivalent if and only if they have submodels with common strong quotients, that is, there exist submodels M′ of M and N′ of N and strong congruences ≃ on M′ and ≃′ on N′ such that the quotients of M′ by ≃ and of N′ by ≃′ are isomorphic.

6. Observational Correctness and Stability

The observational concepts introduced in Sect. 5 above motivate a new interpretation of specifications: for any specification SP with Sig[SP] = Σ, we define its observational interpretation by abstracting from the standard interpretation as follows:

[[SP]]_{≡} = {M ∈ |Mod(Σ)| | M ≡ N for some N ∈ [[SP]]}.

Given this, the most obvious way to re-interpret correctness of local constructions (Def. 3.2) to take advantage of the observational interpretation of specifications is to modify the earlier definition by requiring [[SP]]_{≡} ⊆ dom(F) and F ([[SP]]_{≡}) ⊆ [[SP′]]_{≡}. This works, but misses a crucial point: when using a realization of a specification, we would like to pretend that it satisfies the specification literally, even if when actually implementing it we are permitted to supply a model that is correct only up to observational equivalence. This leads to a different notion of observational correctness of a local construction, for which we would just require [[SP]] ⊆ dom(F) and F ([[SP]]) ⊆ [[SP′]]_{≡}. This relaxation has a price: observationally correct local constructions do not automatically compose! The crucial insight to resolve this problem comes from (Schoett 1987), who noticed that well-behaved constructions satisfy the following stability property.

6.1. Stability

Definition 6.1 (Stability). A construction F: |Mod(Σ)| ⇀ |Mod(Σ′)| is stable if it preserves observational equivalence, i.e., for any models M, N ∈ |Mod(Σ)| such that M ≡ N, if M ∈ dom(F) then N ∈ dom(F) and F (M) ≡ F (N).

The rest of this subsection is devoted to an analysis of conditions that ensure stability of constructions when they arise via the use of local constructions, as in Sect. 3. The problem is that we want to restrict attention to conditions that are essentially local to the local constructions involved, rather than conditions that refer to all the possible global contexts in which such a construction can be used.

Let us start with the local version of the stability property for local constructions, aiming at the stability of any use of local constructions in an admissible global context.

Definition 6.2 (Local stability). A local construction F along ι: Σ → Σ′ is locally stable if for any Σ-models M, N ∈ |Mod(Σ)| and correspondence ρ: M ▷◁ N, M ∈ dom(F) if and only if N ∈ dom(F) and moreover, if this is the case then there exists a correspondence ρ′: F (M) ▷◁ F (N) that extends ρ (i.e., ρ′ _{ι} = ρ).

Clearly, local stability implies stability. Trivial identity constructions are locally stable, and composition of locally stable constructions is locally stable as well. Local stability is also preserved under observational equivalence of constructions:

Local constructions F_{1}, F_{2} along ι: Σ → Σ′ are observationally equivalent, written F_{1} ≡ F_{2}, if dom(F_{1}) = dom(F_{2}) and for each M ∈ dom(F_{1}) there exists a correspondence ρ: F_{1}(M) ▷◁ F_{2}(M) with reduct ρ _{ι} being the identity on M.

Proposition 6.3. Let F_{1} and F_{2} be observationally equivalent local constructions along ι: Σ → Σ′. Then if F_{1} is locally stable then so is F_{2}.

Proof. Consider models M, N ∈ |Mod(Σ)| with correspondence ρ: M ▷◁ N. Suppose M ∈ dom(F_{2}). Then M ∈ dom(F_{1}), and so N ∈ dom(F_{1}) = dom(F_{2}). Since F_{1} is locally stable, there is a correspondence ρ′: F_{1}(M) ▷◁ F_{1}(N) with ρ′ _{ι} = ρ. From F_{1} ≡ F_{2}, we get correspondences ρ_{M}: F_{2}(M) ▷◁ F_{1}(M) and ρ_{N}: F_{1}(N) ▷◁ F_{2}(N) with the identity reducts ρ_{M} _{ι} and ρ_{N} _{ι}. This yields a correspondence (ρ_{M};ρ′;ρ_{N}): F_{2}(M) ▷◁ F_{2}(N) with reduct (ρ_{M};ρ′;ρ_{N}) _{ι} = ρ.

Most crucially though, local stability (unlike stability in general) is preserved under lifting local constructions to a global application context, as usual given by the following pushout diagram:

[figure: Σ; Σ_{G}; Σ′; Σ′_{G}; γ; ι; ι′; γ′]

Lemma 6.4. If F is a locally stable construction along ι: Σ → Σ′ then for any signature Σ_{G} and admissible fitting morphism γ: Σ → Σ_{G}, the induced global construction F_{G}: |Mod(Σ_{G})| ⇀ |Mod(Σ′_{G})| along ι′: Σ_{G} → Σ′_{G} is locally stable as well.

Proof. Consider a correspondence ρ_{G}: G ▷◁ H between models G, H ∈ |Mod(Σ_{G})|. Its reduct is a correspondence ρ_{G} _{γ}: G _{γ} ▷◁ H _{γ}, so G _{γ} ∈ dom(F) iff H _{γ} ∈ dom(F), and consequently G ∈ dom(F_{G}) iff H ∈ dom(F_{G}). Suppose G _{γ} ∈ dom(F). Then there exists a correspondence ρ′: F (G _{γ}) ▷◁ F (H _{γ}) with ρ′ _{ι} = ρ_{G} _{γ}. Amalgamation of ρ_{G} and ρ′ yields a correspondence ρ′_{G}: F_{G}(G) ▷◁ F_{G}(H) such that ρ′_{G} _{ι′} = ρ_{G}, see Lemma 5.6.

Corollary 6.5. If F is a locally stable construction along ι: Σ → Σ′ then for any signature Σ_{G} and admissible fitting morphism γ: Σ → Σ_{G}, the induced global construction F_{G}: |Mod(Σ_{G})| ⇀ |Mod(Σ′_{G})| along ι′: Σ_{G} → Σ′_{G} is stable.

This establishes a sufficient local condition (local stability) which ensures that a local construction induces a stable global construction in every possible context of use. Imposing an additional requirement on the correspondences involved yields an auxiliary notion that we will use to prove that this is both sufficient and necessary.

Given a Casl signature Σ, a correspondence ρ: M ▷◁ N is closed if whenever (a, b) ∈ ρ, (a′, b) ∈ ρ and (a, b′) ∈ ρ, then also (a′, b′) ∈ ρ. The following is easy:

Proposition 6.6. For any correspondence ρ: M ▷◁ N there is a least closed correspondence ρ̂: M ▷◁ N that contains ρ.

Consequently, two Σ-models are behaviourally equivalent iff there is a closed correspondence between them.

Theorem 6.7. For any local construction F along ι: Σ → Σ′, the following conditions are equivalent: 1 F is locally stable; 2 F induces a stable global construction in every possible (also infinitary) context of

use, that is, for every admissible fitting morphism γ: Σ → Σ_{G}, the induced global construction F_{G}: |Mod(Σ_{G})| ⇀ |Mod(Σ′_{G})| along ι′: Σ_{G} → Σ′_{G} is stable; and

3 F extends closed correspondences, that is, for every closed correspondence ρ̂: M ▷◁ N in Mod(Σ), M ∈ dom(F) iff N ∈ dom(F), and if this is the case then there exists a closed correspondence ρ̂′: F (M) ▷◁ F (N) in Mod(Σ′) that extends ρ̂ (i.e., ρ̂′ _{ι} = ρ̂).

Proof. “1 ⟹ 2”: Cor. 6.5.

“2 ⟹ 3”: Consider a closed correspondence ρ̂: M ▷◁ N in Mod(Σ). Construct the extension Σ_{G} of Σ by adding:

— for each sort s in Σ and (a, b) ∈ ρ̂_{s}, a (total) constant !^{a,b,s}: s;

— for each sort s in Σ and b ∈ |N|_{s}, a predicate ?^{b,s}: s; and

— for each sort s in Σ, a predicate ?^{s}: s and let γ: Σ → Σ_{G} be the signature inclusion. The admissibility of γ is easy to check. Construct now the following expansions M_{G} and N_{G} of M and N, respectively:

— for each sort s in Σ and (a, b) ∈ ρ̂_{s}, !_{M_{G}}^{a,b,s} = a and !_{N_{G}}^{a,b,s} = b;

— for each sort s in Σ and b ∈ |N|_{s}, ?_{M_{G}}^{b,s}(a) holds iff (a, b) ∈ ρ̂_{s}; ?_{N_{G}}^{b,s}(b′) holds iff there exists a ∈ |M|_{s} such that (a, b) ∈ ρ̂_{s} and (a, b′) ∈ ρ̂_{s};

— for each sort s in Σ and a ∈ |M|_{s}, ?_{M_{G}}^{s}(a) holds, and for each b ∈ |N|_{s} ?_{N_{G}}^{s}(b) holds iff there exists a ∈ |M|_{s} such that (a, b) ∈ ρ̂_{s}.

It is easy to check that ρ̂: M_{G} ▷◁ N_{G} is a correspondence: closedness of ρ̂: M ▷◁ N is needed to establish that ρ̂ preserves and reflects the ?^{b,s} predicates. Moreover, ρ̂ is the only correspondence between M_{G} and N_{G}: any such correspondence includes ρ̂ because it must preserve the !^{a,b,s} constants, and it is included in ρ̂ because it must preserve and reflect the ?^{b,s} and ?^{s} predicates.

Hence, M_{G} ∈ dom(F_{G}) iff N_{G} ∈ dom(F_{G}), and so also M ∈ dom(F) iff N ∈ dom(F). Moreover, if this is the case then there is a correspondence ρ_{G}: F_{G}(M_{G}) ▷◁ F_{G}(N_{G}) in Mod(Σ′_{G}), and the uniqueness of the correspondence ρ̂: M_{G} ▷◁ N_{G} in Mod(Σ_{G}) implies that ρ_{G} _{ι′} = ρ̂. Consider the least closed correspondence ρ̂_{G}: F_{G}(M_{G}) ▷◁ F_{G}(N_{G}) that includes ρ_{G}. Then we also have ρ̂_{G} _{ι′} = ρ̂, and so we obtain ρ̂_{G} _{γ′}: F (M) ▷◁ F (N) with (ρ̂_{G} _{γ′}) _{ι} = ρ̂.

“3 ⟹ 1”: Consider a correspondence ρ: M ▷◁ N in Mod(Σ). By Prop. 5.4, we have a Σ-model K and strong Σ-homomorphisms h_{M}: K → M and h_{N}: K → N such that ρ = h_{M}^{−1};h_{N}. Since h_{M}^{−1} and h_{N} are closed correspondences, by 3 M ∈ dom(F) iff K ∈ dom(F) iff N ∈ dom(F), and if this is the case then we have correspondences ρ_{M}: F (M) ▷◁ F (K) and ρ_{N}: F (K) ▷◁ F (N) that extend h_{M}^{−1} and h_{N} respectively. Then the correspondence ρ_{M};ρ_{N}: F (M) ▷◁ F (N) extends ρ.

The following is a corollary of Lemma 5.5.

Corollary 6.8. Let δ: Σ′ → Σ be an observationally sensible derived signature morphism and ι: Σ → Σ′ be a signature morphism such that ι;δ = id_{Σ}. Then the reduct

δ: |Mod(Σ)| → |Mod(Σ′)| is a local construction that is locally stable.

The above corollary supports the point put forward in (Schoett 1987) that stable constructions are those that respect modularity in the software construction process. That is, such constructions can use the components provided by their imported parameters, but they cannot take advantage of their particular internal properties. This is the point of the requirement that δ should be observationally sensible: any branching in the code must be governed by directly observable properties. This turns (local) stability into a directive for language design, rather than a condition to be checked on a case-by-case basis: in a language with good modularization facilities, all constructions that one can code should be locally stable.

6.2. Observational correctness

Let us turn now again to the issue of correctness of local constructions w.r.t. given specifications.

Definition 6.9 (Observational correctness). A local construction F along ι: Sig[SP] → Sig[SP′] is observationally correct w.r.t. SP and SP′ if for every model M ∈ [[SP]], M ∈ dom(F) and there exists a model M′ ∈ [[SP′]] and correspondence ρ′: M′ ▷◁ F (M) such that ρ′ _{ι} is the identity.

We write [[SP⟶^{ι}SP′]]_{≡} for the class of all locally stable constructions along ι that are observationally correct w.r.t. SP and SP′.

By imposing in this definition the restriction that ρ′ is the identity on the carriers of the parameter sorts, we have in fact “locally” introduced a set of sorts that act as directly observable for the purposes of verification of the local construction considered.

It follows that if F ∈ [[SP⟶^{ι}SP′]]_{≡} then there is some F′ ∈ [[SP⟶^{ι}SP′]] such that dom(F′) = dom(F) and for each M ∈ [[SP]], there is a correspondence ρ: F′(M) ▷◁ F (M) which is the identity on sorts of the form ι(s) for s in Σ. However, in general [[SP⟶^{ι}SP′]] ⊈ [[SP⟶^{ι}SP′]]_{≡}, as literally correct local constructions need not be stable. Moreover, it may happen that there are no stable observationally correct constructions, even if there are literally correct ones: that is, we may have [[SP⟶^{ι}SP′]]_{≡} = ∅ even if [[SP⟶^{ι}SP′]] ≠ ∅. This was perhaps first pointed out in (Bernot 1987), in a different framework.

Counterexample 6.10. Let SP_{1} have a sort s with two constants a, b: s, and let SP_{2} enrich SP_{1} by a new sort o with predicate p : o × o, two (total) constants c, d: o and axiom p(c, d) ⟺ a = b. Then [[SP_{1} → SP_{2}]] is non-empty, with any construction in it mapping models satisfying a = b to those that satisfy p(c, d), and models satisfying a ≠ b to those that do not satisfy p(c, d). But none of these constructions is stable!

To see this, consider any construction F ∈ [[SP_{1}⟶^{ι}SP_{2}]], “singleton” model M ∈ [[SP_{1}]] (where a_{M} = b_{M}) and two-element model N ∈ [[SP_{2}]] with a_{N} ≠ b_{N}. Clearly, M ≡ N. However, there is no correspondence between F (M) and F (N): it would have to link c_{F (M)} with c_{F (N)} and d_{F (M)} with d_{F (N)}, which is impossible since F (M) ⊧ p(c, d) while F (N) |̸= p(c, d).

The crucial issue here is how specifications of local constructions can be used when the local constructions are lifted to an admissible global context, captured by the following pushout diagram:

[figure: Sig[SP]; Σ_{G}; Sig[SP′]; Σ′_{G}; γ; ι; ι′; γ′]

Lemma 6.11. Consider a local construction F along ι: Sig[SP] → Sig[SP′] that is observationally correct w.r.t. SP and SP′, F ∈ [[SP⟶^{ι}SP′]]_{≡}. Then, for every global signature Σ_{G} and admissible fitting morphism γ: Sig[SP] → Σ_{G}, and every G ∈ [[SP with γ]] we have G ∈ dom(F_{G}) and there is some G′ ∈ [[SP′ with γ′]] such that G′ _{ι′} = G and G′ ≡ F_{G}(G).

Proof. We have G _{γ} ∈ [[SP]], and so G _{γ} ∈ dom(F) and there is M′ ∈ [[SP′]] and a correspondence ρ′: M′ ▷◁ F (G _{γ}) with identity reduct ρ′ _{ι}. Consider the Σ′_{G}-model G′ = G ⊕ M′. Then the identity id_{G}: G ▷◁ G and ρ′: M′ ▷◁ F (G _{γ}) amalgamate to a correspondence ρ′_{G}: G′ ▷◁ F_{G}(G), which proves F_{G}(G) ≡ G′ ∈ [[SP′ with γ′]].

If F ∈ [[SP⟶^{ι}SP′]]_{≡} and γ: Sig[SP] → Σ_{G} is admissible, then by Lemma 6.11 we obtain [[SP with γ]] ⊆ dom(F_{G}) and F_{G}([[SP with γ]]) ⊆ [[SP′ with γ′]]_{≡}, and by Cor. 6.5, F_{G} is stable. Given two “global” specifications SP_{G} with Sig[SP_{G}] = Σ_{G} and SP′_{G} with Sig[SP′_{G}] = Σ′_{G}, we have F_{G} ∈ [[SP_{G}⟶^{ι′}SP′_{G}]]_{≡} whenever [[SP_{G}]] ⊆ [[SP with γ]]_{≡} and [[SP′ with γ′]] ⊆ [[SP′_{G}]]_{≡}. But while the former requirement is quite acceptable, the latter is in fact impossible to achieve in practice since it implicitly requires that all the global requirements must follow (up to observational equivalence) from the result specification for the local construction, independent of the argument. More practical requirements are obtained by generalizing Thm. 3.4 to the observational setting:

Theorem 6.12. Given a local construction F ∈ [[SP⟶^{ι}SP′]]_{≡}, a specification SP_{G} with admissible fitting morphism γ: Sig[SP] → Sig[SP_{G}], and a specification SP′_{G} with Sig[SP′_{G}] = Σ′_{G}, if

(i) [[SP_{G}]] ⊆ [[SP_{G} and (SP with γ)]]_{≡}, and (ii) [[(SP′ with γ′) and (SP_{G} with ι′)]] ⊆ [[SP′_{G}]]_{≡} then for every G ∈ [[SP_{G}]], we have G ∈ dom(F_{G}) and F_{G}(G) ∈ [[SP′_{G}]]_{≡}, hence F_{G} ∈

[[SP_{G}⟶^{ι′}SP′_{G}]]_{≡}.

Proof. Let G ∈ [[SP_{G}]]. Then G ≡ H for some H ∈ [[SP_{G}]] ∩ [[SP with γ]] by (i). By Lemma 6.11, F_{G}(H) ≡ H′ for some H′ ∈ [[SP′ with γ′]] with H′ _{ι′} = H ∈ [[SP_{G}]]. Hence H′ ∈ [[SP′_{G}]]_{≡} by (ii). By stability of F_{G} (Cor. 6.5), G ∈ dom(F_{G}) and F_{G}(G) ≡ F_{G}(H) ≡ H′, and so F_{G}(G) ∈ [[SP′_{G}]]_{≡}. This completes the proof, since F_{G} is locally stable by Lemma 6.4.

Requirement (i) is perhaps the only surprising assumption in this theorem. Note though that it straightforwardly follows from the inclusion of literal model classes [[SP_{G}]] ⊆ [[SP with γ]] (or equivalently, [[SP_{G}]] _{γ} ⊆ [[SP]]), which is often easiest to verify. However,

(i) is strictly stronger in general than the perhaps more expected [[SP_{G}]] ⊆ [[SP with γ]]_{≡}. This weaker condition turns out to be sufficient (and is in fact equivalent to (i)) if we additionally assume that the two specifications involved are behaviourally consistent (Bidoit, Hennicker and Wirsing 1995), that is, closed under observational quotients. When this is not the case, then the use of this weaker condition would have to be paid for by a stronger version of (ii):

[[SP′ with γ′]]_{≡} ∩ [[SP_{G} with ι′]] ⊆ [[SP′_{G}]]_{≡},

which seems even less convenient to use than (i). Overall, we need a way to pass information on the global context from SP_{G} to SP′_{G} independently from the observational interpretation of the local construction and its correctness, and this must result in some inconvenience of verification on either the parameter or the result side.

7. Observational Interpretation of Architectural Specifications

In this section we discuss an observational interpretation of the architectural specifications introduced in Sect. 4. The extended static semantics remains unchanged — observational interpretation of specifications does not affect their static properties. We provide, however, a new observational model semantics, with judgments written as ⊢ ⟹^{≡} .

To begin with, the effect of unit declarations has to be modified, taking into account observational interpretation of the specifications involved, as discussed in Sects. 5 and 6. The new rules follow in Fig. 4. No other modifications are necessary: all the remaining rules are the same for observational and literal model semantics. This should not be surprising: the interpretation of the constructs on unit terms remains the same, all we change is the interpretation of unit specifications. Moreover, the observational model semantics can be linked to the extended static semantics in exactly the same way as in the case of the literal model semantics: the invariants stated in Thm. 4.2 carry over

\overline{C ⊢ U : SP ⟹^{≡} C × \{U ↦ [[SP]]_{≡}\}}

C ⊢ U : SP_{1}⟶^{ι}SP_{2} ⟹^{≡} C × {U ↦ [[SP_{1}⟶^{ι}SP_{2}]]_{≡}}

Fig. 4. Observational model semantics — the modified rules

without change. We refrain from repeating either the unmodified rules, or Thm. 4.2 for the observational model semantics.

The fact that nearly all the rules remain the same does not mean that the two semantics quite coincide: at the point in the model semantics where verification is performed, the resulting verification conditions for literal and observational model semantics differ. Namely, in the rule for parametrized unit application, the premise

for each E ∈ C, UEv(E) _{γ} ∈ dom(E(U ))

checks whether what we can conclude about the argument ensures that it is indeed in the domain of the parametrized unit. Suppose the corresponding unit declaration was U : SP_{1}⟶^{ι}SP_{2}. Then in the literal model semantics this requirement reduces to

for each E ∈ C, UEv(E) _{γ} ∈ [[SP_{1}]].

Now, in the observational model semantics, this is in fact replaced by a more permissive condition (since the parametrized units considered are locally stable, their domains are closed under observational equivalence):

for each E ∈ C, UEv(E) _{γ} ∈ [[SP_{1}]]_{≡}.

Of course, the situation is complicated by the fact that the contexts C from which environments are taken are different in the two semantics. In the simplest case, where the argument T is given as a unit name previously declared with a specification SP, for the literal model semantics the above verification condition amounts to [[SP]] ⊆ [[SP_{1}]] while for the observational model semantics we get, as expected, [[SP]] ⊆ [[SP_{1}]]_{≡} (which is equivalent to [[SP]]_{≡} ⊆ [[SP_{1}]]_{≡}).

This relaxation of verification conditions is not of merely theoretical interest: it is not difficult to find statically correct architectural specifications ASP (i.e., ⊢ ASP ⊳ ⊳ (C_{st}, Σ) for some extended static context C_{st} and signature Σ) that are observationally correct (i.e., ⊢ ASP ⟹^{≡} (C_{♭}, UEv_{♭}) for some unit context C_{♭} and evaluator UEv_{♭}) but are not literally correct (i.e., for no unit context C and evaluator UEv can we derive ⊢ ASP ⇒ (C, UEv)). For instance, along the lines of the discussion above, one may take

arch spec ASP =

units \begin{matrix}U : SP_{1}⟶^{ι}SP_{2}; \\ T : SP \end{matrix}

result U [T]

where Sig[SP] = Sig[SP_{1}], [[SP]] ⊆ [[SP_{1}]]_{≡} but [[SP]] ⊈ [[SP_{1}]].

A complete study of verification conditions for architectural specifications is beyond the scope of this paper; we refer to (Hoffman 2001; Mossakowski et al. 2004) for work in this direction, which still has to be combined with the observational interpretation as given by the semantics here and presented in the simpler setting of Sect. 6. In the rest of this paper we will concentrate on some aspects of the relationship between the literal and observational model semantics and on stability of the unit constructions introduced in Sect. 4.

Our first aim is to show that constructions that can be defined by architectural specifications are (locally) stable. To state this precisely, we need some more notation and terminology, as constructions are captured here by unit evaluators operating on environments rather than on individual units.

For any extended static context C_{st} = (P_{st}, B_{st}, D), environments E_{1}, E_{2} ∈ ucx(C_{st}) are observationally equivalent in C_{st}, written E_{1} ≡_{C_{st}} E_{2}, if for each unit name U in C_{st}, E_{1}(U ) ≡ E_{2}(U ). A unit environment E ∈ ucx(C_{st}) is stable in C_{st} if for each parametrized unit name U in C_{st}, E(U ) is locally stable. By Prop. 6.3, the class of environments that are stable in C_{st} is closed under observational equivalence in C_{st}. We write ucx_{♭}(C_{st}) for the class of all unit environments that fit C_{st} and are stable in C_{st}.

A D-coherent correspondence between D-coherent model families M^{1}, M^{2} ∈ |Mod(D)|, written ρ: M^{1} ▷◁ M^{2}, is a family of correspondences ρ_{i}: M_{i}^{1} ▷◁ M_{i}^{2} for i ∈ |D| such that ρ_{i} = ρ_{j} _{D(m)} for each m: i → j in D.

Two unit environments E_{1}, E_{2} ∈ ucx_{♭}(C_{st}) are coherently equivalent in C_{st}, written E_{1} ▷◁_{C_{st}} E_{2}, if for all parametrized unit names U in C_{st}, E_{1}(U ) ≡ E_{2}(U ), and there are Dcoherent families of models M_{1} and M_{2} with a D-coherent correspondence ρ: M_{1} ▷◁ M_{2} such that M_{1} and M_{2} witness E_{1} and E_{2} respectively in C_{st}.

Then, given a unit context C ⊆ ucx(C_{st}), we write Cl_{≡}^{C_{st}} (C) for the class of all unit environments that in C_{st} are stable and coherently equivalent to a unit environment in C. Clearly then Cl_{≡}^{C_{st}} (C) ⊆ ucx_{♭}(C_{st}).

Back to the stability of the constructions defined by architectural specifications: we want to show that if ⊢ ASP ⊳ ⊳ (C_{st}, Σ) and ⊢ ASP ⟹^{≡} (C_{♭}, UEv_{♭}) then the unit evaluator UEv_{♭} is stable, i.e., maps observationally equivalent environments to observationally equivalent models. Unfortunately, this cannot be proved by a simple induction on the structure of the unit terms involved, relying on the fact that (locally) stable constructions are closed under composition. The trouble is with amalgamation, since in general amalgamation is not stable — informally, joining the signatures of two models may introduce new observations for either or both of them, see Counterexample 5.7.

However, the key point here is that amalgamation in unit terms in architectural specifications is not used as a construction on its own, but it just identifies a new part of the global context that has been constructed earlier. Since the constructions used to build genuinely new components of the global context are locally stable, such use of amalgamation can cause no harm.

The following lemma captures the essential stability property of the unit evaluators built for unit terms by the observational model semantics.

Lemma 7.1. Assume C_{st} ⊢ T ⊳ ⊳ (i, D′) and C_{♭} ⊢ T ⟹^{≡} UEv_{♭} with C_{♭} ⊆ ucx_{♭}(C_{st}), where C_{st} = (P_{st}, B_{st}, D). The unit evaluator UEv_{♭} is locally stable in the following sense:

Consider any E_{1}, E_{2} ∈ C_{♭} such that E_{1} ▷◁_{C_{st}} E_{2}, and M_{1}, M_{2} ∈ |Mod(D)| that witness E_{1} and E_{2} respectively in C_{st}. Any D-coherent correspondence ρ: M^{1} ▷◁ M^{2} can be extended to a D′-coherent correspondence ρ′: M′_{1} ▷◁ M′_{2} between model families M′_{1}, M′_{2} ∈ |Mod(D′)| that extend M_{1} and M_{2} respectively and satisfy (M′_{1})_{i} = UEv_{♭}(E_{1}) and (M′_{2})_{i} = UEv_{♭}(E_{2}).

Proof. By induction on the structure of the unit term. The cases when the term is a unit name or a unit reduction are trivial.

Consider the case of parametrized unit application. Using the notation as in the corresponding rules of the extended static semantics and of the (observational) model semantics in Figs. 1 and 3 respectively, consider E_{1}, E_{2} ∈ C_{♭} such that E_{1} ▷◁_{C_{st}} E_{2} and a coherent correspondence ρ: M_{1} ▷◁ M_{2} between model families M^{1}, M^{2} that witness E_{1} and E_{2} respectively in C_{st}. By the inductive hypothesis, ρ can be extended to a Dcoherent correspondence ρ^{T} : M_{1}^{T} ▷◁ M_{2}^{T} , where M_{1}^{T} extends M_{1}, M_{2}^{T} extends M_{2}, (M_{1}^{T} )_{i} = UEv(E_{1}) and (M_{2}^{T} )_{i} = UEv(E_{2}). Then, ρ^{T} extends to a D′-coherent correspondence ρ′: M′_{1} ▷◁ M′_{2}, where (M′_{1})_{j} = UEv(E_{1}) _{γ}, (M′_{1})_{k} = E_{1}(U )(UEv(E_{1}) _{γ}), and similarly for M′_{2} (by local stability of either E_{1}(U ) or E_{2}(U ), and the fact that E_{1}(U ) ≡ E_{2}(U )). Now, we can extend M′_{1} and M′_{2} to D′′-coherent model families M′′_{1} and M′′_{2}, respectively, by putting (M′′_{1})_{l} = UEv(E_{1}) _{γ} ⊕ E_{1}(U )(UEv(E_{1}) _{γ}), and similarly for M′′_{2}. Moreover, similarly as in Lemma 5.6, following the proof of Lemma 2.2, we can extend ρ′ to a coherent correspondence ρ′′: M′′_{1} ▷◁ M′′_{2}.

Finally, consider the case of unit amalgamation. Using the notation as in the corresponding rules of the extended static semantics and of the (observational) model semantics in Figs. 1 and 3 respectively, consider E_{1}, E_{2} ∈ C_{♭} such that E_{1} ▷◁_{C_{st}} E_{2} and a coherent correspondence ρ: M_{1} ▷◁ M_{2} between model families M_{1}, M_{2} that witness E_{1} and E_{2} respectively in C_{st}. By the inductive hypothesis, ρ can be extended to a D_{1}- coherent correspondence ρ^{T_{1}}: M_{1}^{T_{1}} ▷◁ M_{2}^{T_{1}}, where (M_{1}^{T_{1}}) extends M_{1}, (M_{2}^{T_{1}}) extends M_{2}, (M_{1}^{T_{1}})_{i} = UEv_{1}(E_{1}) and (M_{2}^{T_{1}})_{i} = UEv_{1}(E_{2}). Similarly, ρ can be extended to a D_{2}-coherent correspondence ρ^{T_{2}}: M_{1}^{T_{2}} ▷◁ M_{2}^{T_{2}}, where (M_{1}^{T_{2}}) extends M_{1}, (M_{2}^{T_{2}}) extends M_{2}, (M_{1}^{T_{2}})_{i} = UEv_{2}(E_{1}) and (M_{2}^{T_{2}})_{i} = UEv_{2}(E_{2}). Now, since D_{1} and D_{2} are disjoint extensions of D, ρ^{T_{1}} and ρ^{T_{2}} can be put together to form a (D_{1} ∪ D_{2})-coherent correspondence between M_{1}^{T_{1}} ∪ M_{1}^{T_{2}} and M_{2}^{T_{1}} ∪ M_{2}^{T_{2}} respectively. To complete the proof we proceed as in the previous case, following Lemma 5.6 generalized as indicated in footnote 7; this is possible since the union of Casl signatures is built by taking the union of their respective sets of sort, operation and predicate names and forming the transitive closure of the union of the subsort preorders. Consequently, no new sorts, operations or predicates are added in the resulting model; everything there was constructed “earlier” while evaluating T_{1} and T_{2}.

We can strengthen the invariant concerning the semantics of unit declarations and definitions by adding the following property:

Corollary 7.2. Let C_{st} ⊢ UDD ⊳ ⊳ C′_{st} and C_{♭} ⊢ UDD ⟹^{≡} C′_{♭} with C_{♭} ⊆ ucx_{♭}(C_{st}). Then C′_{♭} ⊆ ucx_{♭}(C′_{st}), C′_{♭} ⊆ C_{♭}, and for any unit environments E′_{1}, E′_{2} ∈ C′_{♭} such that E′_{1} ≡_{C′_{st}} E′_{2}, whenever E′_{1} ▷◁_{C_{st}} E′_{2} then also E′_{1} ▷◁_{C′_{st}} E′_{2}.

Proof. This follows by easy inspection of the rules, using Lemma 7.1 for the case of unit definitions.

Corollary 7.3. Let ⊢ UDD^{+} ⊳ ⊳ C_{st} and ⊢ UDD^{+} ⟹^{≡} C_{♭}. Then C_{♭} ⊆ ucx_{♭}(C_{st}) and for any unit environments E_{1}, E_{2} ∈ C_{♭} if E_{1} ≡_{C_{st}} E_{2} then also E_{1} ▷◁_{C_{st}} E_{2}.

Proof. For the empty extended static context C_{st}^{∅}, any environment in C^{∅} is witnessed by the empty family of models, and so any such two environments are coherently equivalent in C_{st}^{∅}. Therefore, by Cor. 7.2 and an easy induction on the length of the sequence of unit declaration and definitions, for any E_{1}, E_{2} ∈ C_{♭} such that E_{1} ≡_{C_{st}} E_{2} as in the premise of the corollary, we have E_{1} ▷◁_{C_{st}} E_{2}.

Corollary 7.4. If ⊢ ASP ⊳ ⊳ (C_{st}, Σ) and ⊢ ASP ⟹^{≡} (C_{♭}, UEv_{♭}) then C_{♭} ⊆ ucx_{♭}(C_{st}) and for any unit environments E_{1}, E_{2} ∈ C_{♭} such that E_{1} ≡_{C_{st}} E_{2}, we have UEv_{♭}(E_{1}) ≡ UEv_{♭}(E_{2}).

Proof. By Cor. 7.3 we have that for any E_{1}, E_{2} ∈ C_{♭} such that E_{1} ≡_{C_{st}} E_{2} as in the premise here, E_{1} ▷◁_{C_{st}} E_{2}. The conclusion follows by the stability property in Lemma 7.1.

As already mentioned, the observational semantics is more permissive than the literal model semantics: the existence of a successful derivation of an observational meaning for an architectural specification does not in general imply that its literal model semantics is defined. Moreover, the observational semantics may “lose” some results permitted by the literal model semantics, see Counterexample 6.10. However, if an architectural specification has a literal model semantics then its observational semantics is defined as well and up to observational equivalence, nothing new is added. The following theorem captures the essential links between literal model semantics and observational model semantics.

Theorem 7.5. The following relationships between literal and observational model semantics hold: 1 If ⊢ ASP ⊳ ⊳ ((P_{st}, B_{st}), Σ) and ⊢ ASP ⇒ (C, UEv) then ⊢ ASP ⟹^{≡} (C_{♭}, UEv_{♭})

with C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) and for each unit environment E ∈ C that is stable in C_{st}, E ∈ C_{♭} and UEv_{♭}(E) = UEv(E).

2 If ⊢ UDD^{+} ⊳ ⊳ C_{st} and ⊢ UDD^{+} ⇒ C then ⊢ UDD^{+} ⟹^{≡} C_{♭}, where C_{♭} ⊆ Cl_{≡}^{C_{st}} (C)

and C_{♭} contains all unit environments E ∈ C that are stable in C_{st}. 3 If C_{st} ⊢ UDD ⊳ ⊳ C′_{st} and C ⊢ UDD ⇒ C′, where C ⊆ ucx(C_{st}), then for any

C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) that contains all unit environments E ∈ C that are stable in C_{st}, C_{♭} ⊢ UDD ⟹^{≡} C′_{♭}, where C′_{♭} ⊆ Cl_{≡}^{C′_{st}} (C′) and C′_{♭} contains all unit environments E′ ∈ C′ that are stable in C′_{st}.

4 If C_{st} ⊢ T ⊳ ⊳ (i, D′) and C ⊢ T ⇒ UEv with C ⊆ ucx(C_{st}) then for any C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) that contains all unit environments E ∈ C that are stable in C_{st}, C_{♭} ⊢ T ⟹^{≡} UEv_{♭} and for E ∈ C ∩ C_{♭}, UEv_{♭}(E) = UEv(E).

Proof. Item 4 follows by induction on the structure of the unit term. As usual, the cases when the term is a unit name or a unit reduction are easy.

Consider the case of unit application, when the unit term is of the form U [T fit γ]. Assume then C ⊆ ucx(C_{st}), C_{st} ⊢ U [T fit γ] ⊳ ⊳ (l, D′′) and C ⊢ U [T fit γ] ⇒ UEv′, with UEv′(E) = UEv(E) ⊕ E(U )(UEv(E) _{γ}) for E ∈ C. Consequently, all the premises of the corresponding rules (for unit application) in Figs. 1 and 3 must hold; we refer below to the notations used in the rules. Take now any C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) that contains all unit environments E ∈ C that are stable in C_{st}. By the inductive hypothesis, C_{♭} ⊢ T ⟹^{≡} UEv_{♭} and for E ∈ C ∩ C_{♭}, UEv_{♭}(E) = UEv(E). Consider now any E_{♭} ∈ C_{♭} ⊆ Cl_{≡}^{C_{st}} (C), with some E ∈ C such that E_{♭} ▷◁_{C_{st}} E. Then E ∈ C ∩ C_{♭}. We have E_{♭}(U ) ≡ E(U ), UEv_{♭}(E) = UEv(E), and since by Lemma 7.1 UEv(E) ≡ UEv(E_{♭}) and observational equivalence is preserved by reducts, from UEv(E) _{γ} ∈ dom(E(U )) we obtain UEv_{♭}(E_{♭}) _{γ} ∈ dom(E_{♭}(U )). Thus, we can derive C_{♭} ⊢ U [T fit γ] ⟹^{≡} UEv′_{♭}, where for E_{♭} ∈ C_{♭}, UEv′_{♭}(E_{♭}) = UEv_{♭}(E_{♭}) ⊕ E_{♭}(U )(UEv_{♭}(E_{♭}) _{γ}). Now, for E ∈ C ∩ C_{♭}, since UEv_{♭}(E) = UEv(E), it follows that UEv′_{♭}(E) = UEv′(E) — which completes the proof for this case.

The proof for the case of unit amalgamation, when the unit term is of the form T_{1} and T_{2}, proceeds quite similarly: assume C ⊆ ucx(C_{st}), C_{st} ⊢ T_{1} and T_{2} ⊳ ⊳ (j, D′) and C ⊢ T_{1} and T_{2} ⇒ UEv. Consequently, all the premises of the corresponding rules (for unit amalgamation) in Figs. 1 and 3 must hold; we refer below to the notations used in the rules. Take now any C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) that contains all unit environments E ∈ C that are stable in C_{st}. By the inductive hypothesis, C_{♭} ⊢ T_{1} ⟹^{≡} UEv_{♭}^{1}, C_{♭} ⊢ T_{2} ⟹^{≡} UEv_{♭}^{2}, and for E ∈ C ∩ C_{♭}, UEv_{♭}^{1}(E) = UEv_{1}(E) and UEv_{♭}^{2}(E) = UEv_{2}(E). Then C_{♭} ⊢ T_{1} and T_{2} ⟹^{≡} UEv_{♭}, where for E_{♭} ∈ C_{♭}, UEv_{♭}(E_{♭}) amalgamates UEv_{♭}^{1}(E_{♭}) and UEv_{♭}^{2}(E_{♭}). Clearly now, by the definition of UEv in the model semantics, for E ∈ C ∩ C_{♭}, since UEv_{♭}^{1}(E) = UEv_{1}(E) and UEv_{♭}^{2}(E) = UEv_{2}(E), we conclude that UEv_{♭}(E) = UEv(E) — which completes the proof of item 4.

Item 3 follows by inspection of the rules; the cases of unit declarations are easy. The case of unit definition relies on item 4 as follows. Assume that C ⊆ ucx(C_{st}) and C is closed in C_{st} = (P_{st}, B_{st}, D). To derive C_{st} ⊢ UDD ⊳ ⊳ C′_{st} and C ⊢ UDD ⇒ C′, where UDD is of the form U = T , we must have (P_{st}, B_{st}, D) ⊢ T ⊳ ⊳ (i, D′), U ∉ (dom(P_{st}) ∪ dom(B_{st})), and C ⊢ T ⇒ UEv, with C′_{st} = (P_{st}, B_{st} + {U ↦ i}, D′) and C′ = {E + {U ↦ UEv(E)} | E ∈ C}. Take now any C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) that contains all unit environments E ∈ C that are stable in C_{st}. By item 4, C_{♭} ⊢ T ⟹^{≡} UEv_{♭} and for E ∈ C ∩ C_{♭}, UEv_{♭}(E) = UEv(E). Hence, C_{♭} ⊢ U = T ⇒ C′_{♭} with C′_{♭} = {E_{♭} + {U ↦ UEv_{♭}(E_{♭})} | E_{♭} ∈ C_{♭}}. To see that C′_{♭} ⊆ Cl_{≡}^{C′_{st}} (C′), consider any E_{♭} ∈ C_{♭} ⊆ Cl_{≡}^{C_{st}} (C), with some E ∈ C such that E_{♭} ▷◁_{C_{st}} E. By Lemma 7.1, E_{♭}+{U ↦ UEv_{♭}(E_{♭})} is coherently equivalent in C′_{st} to E +{U ↦ UEv_{♭}(E)}, which is the same as E + {U ↦ UEv(E)}. This shows that E_{♭} + {U ↦ UEv_{♭}(E_{♭})} is indeed in Cl_{≡}^{C′_{st}} (C′). Finally, if for some E ∈ C, E + {U ↦ UEv(E)} is stable in C′_{st}, then E is stable in C_{st} and so is in C_{♭}. Since then UEv_{♭}(E) = UEv(E) by item 4, we also have that E + {U ↦ UEv(E)} is in C′_{♭}.

Item 2 follows from item 3 by an easy induction on the length of the sequence of unit declarations and definitions. To start, notice that every environment in C^{∅} is stable in the empty static context C_{st}^{∅} and is witnessed in C_{st}^{∅} by the empty family of models; hence, C^{∅} = Cl_{≡}^{C_{st}^{∅}} (C^{∅}).

Item 1 now follows easily: to derive the assumptions for ASP of the form arch spec UDD^{+} result T , we must have ⊢ UDD^{+} ⊳ ⊳ C_{st} and ⊢ UDD^{+} ⇒ C, as well as C_{st} ⊢ T ⊳ ⊳ and C ⊢ T ⇒ UEv, with (P_{st}, B_{st}) = ctx(C_{st}) and Σ = D(i). By item 2 we thus have ⊢ UDD^{+} ⟹^{≡} C_{♭}, where C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) and C_{♭} contains all unit environments E ∈ C that are stable in C_{st}. By item 4 in turn, C_{♭} ⊢ T ⟹^{≡} UEv_{♭} and for each unit environment E ∈ C stable in C_{st}, UEv_{♭}(E) = UEv(E) (since E ∈ C ∩ C_{♭} then).

Corollary 7.6. If ⊢ ASP ⊳ ⊳ (C_{st}, Σ) and ⊢ ASP ⇒ (C, UEv) then ⊢ ASP ⟹^{≡} (C_{♭}, UEv_{♭}), where for every E_{♭} ∈ C_{♭} there exists E ∈ C such that E_{♭} ≡_{C_{st}} E and UEv_{♭}(E_{♭}) ≡ UEv(E).

Proof. Given the assumptions, by Thm. 7.5, ⊢ ASP ⟹^{≡} (C_{♭}, UEv_{♭}) with C_{♭} ⊆ Cl_{≡}^{C_{st}} (C) and for each E ∈ C that is stable in C_{st}, E ∈ C_{♭} and UEv_{♭}(E) = UEv(E). Hence, for each E_{♭} ∈ C_{♭} there is a stable environment E ∈ C such that E_{♭} ▷◁_{C_{st}} E and UEv(E) = UEv_{♭}(E). It follows that E_{♭} ≡_{C_{st}} E and, by Cor. 7.4, UEv_{♭}(E) ≡ UEv_{♭}(E_{♭}), which yields UEv(E) ≡ UEv_{♭}(E_{♭}).

8. Example

The following example illustrates some of the points in the paper. The notation of Casl is hopefully understandable without further explanation; otherwise see (CoFI 2004).

We start with a simple specification of sets of strings; we will not go into any details of a specification of strings, just remarking that any standard specification would typically be monomorphic (with a unique model, up to isomorphism) and would certainly provide the equality predicate for strings.

spec String = sort String ⋯ pred eq_{S} : String × String; axiom ∀s, s′ : String • eq_{S}(s, s′) ⟺ s = s′ ⋯

spec StringSet = String then

sort Set

ops empty : Set;

add : String × Set → Set pred present : String × Set ∀ s, s′ : String, t : Set

• add(s, add(s, t)) = add(s, t)

• add(s, add(s′, t)) = add(s′, add(s, t))

• ¬present(s, empty)

• present(s, add(s, t))

• s ≠ s′ ⟹ (present(s, add(s′, t)) ⟺ present(s, t))

We now provide a more elaborate version of the requirements this specification captures, introducing the idea of using a hash table implementation of sets.

M. Bidoit, D. Sannella and A. Tarlecki 36

spec Int = sort Int ⋯ pred eq_{N} : Int × Int; axiom ∀n, n′ : Int • eq_{N}(n, n′) ⟺ n = n′ ⋯

spec Elem = sort Elem

spec Array[Elem] = Elem and Int then

sort Array[Elem]

ops empty : Array[Elem]; put : Int × Elem × Array[Elem] → Array[Elem]; take : Int × Array[Elem] →? Elem

pred used : Int × Array[Elem] ∀ i, j : Int; e, e′ : Elem; a : Array[Elem]

• i ≠ j ⟹ put(i, e′, put(j, e, a)) = put(j, e, put(i, e′, a))

• put(i, e′, put(i, e, a)) = put(i, e′, a)

• ¬used(i, empty)

• used(i, put(i, e, a))

• i ≠ j ⟹ ( used(i, put(j, e, a)) ⟺ used(i, a) )

• take(i, put(i, e, a)) = e

spec ElemKey = Elem and Int then op hash : Elem → Int

spec HashTable[ElemKey] = ElemKey and Array[Elem]

then ops add : Elem × Array[Elem] → Array[Elem];

putnear : Int × Elem × Array[Elem] → Array[Elem] preds present : Elem × Array[Elem]

isnear : Int × Elem × Array[Elem] ∀ i : Int; e : Elem; a : Array[Elem]

• add(e, a) = putnear(hash(e), e, a)

• ¬used(i, a) ⟹ putnear(i, e, a) = put(i, e, a)

• used(i, a) ∧ take(i, a) = e ⟹ putnear(i, e, a) = a • used(i, a) ∧ take(i, a) ≠ e ⟹ putnear(i, e, a) = putnear(succ(i), e, a)

• present(e, a) ⟺ isnear(hash(e), e, a)

• ¬used(i, a) ⟹ ¬isnear(i, e, a)

• used(i, a) ∧ take(i, a) = e ⟹ isnear(i, e, a)

• used(i, a) ∧ take(i, a) ≠ e ⟹ (isnear(i, e, a) ⟺ isnear(succ(i), e, a))

spec StringKey = String and Int then op hash : String → Int

spec StringHashTable =

HashTable[StringKey] with Array[String] ↦ Set reveal String, Set, empty, add, present

StringHashTable does not literally ensure all the requirements imposed by the original specification StringSet: the second axiom (commutativity of adding elements to a set) fails in some models of StringHashTable. Still, it is easy to check that [[StringHashTable]] ⊆ [[StringSet]]_{≡} and so every future (observationally-correct) realisation of StringHashTable is an observationally-correct realisation of StringSet.^{10}

StringHashTable is structured in a fairly natural way, building on a generic specification of arrays that is presumably already available, and including a generic specification of hash tables that may be reused in the future.

However, the structure of StringHashTable must not be viewed as an obligatory prescription of the structure of the final implementation. For example, we may decide to adopt the different structure given below by the architectural specification StringHashTableDesign.

The architectural specification uses the Casl construct given to mark units that are imported by other units. Formally, a sequence of declarations like

N : Int; S : String;

SK : StringKey given S, N;

abbreviates

N : Int; S : String;

SK′ : Int × String → StringKey; SK = SK′[N][S];

where a new generic construction SK′ is introduced and immediately applied to the imported units.

arch spec StringHashTableDesign =

units N : Int; S : String; SK : StringKey given S, N; A : Elem → Array[Elem] given N; ASK = A[SK fit Elem ↦ String]; HT : StringHashTable

given {ASK with Array[String] ↦ Set}

result HT reveal String, Set, empty, add, present

The above architectural specification captures a modular design of the system to be built as follows. Components N and S are to be defined, implementing specifications Int and String, respectively. Presumably, these would be predefined in any practical programming language. Then, N and S are put together and extended by a definition of a hash function hash, yielding a new component SK . However, as explained above, the given notation used here really means that we are to provide a construction (a generic unit SK′) that yields such a component for any realisations of Int and String. Another component to be provided is a generic unit A to implement arrays indexed by integers and storing data of any sort (Elem, to be instantiated when A is applied to an argument component). Again, this is to be given by a construction A′ that works for any implementation of Int, but then is instantiated with the specific implementation given by N. This is then used to build a component ASK , that implements arrays of strings (with a hash function) by instantiating A with SK . In turn, ASK (with the

10 Note that dropping the first two axioms in StringSet yields a specification with a class of models that coincides with [[StringSet]]_{≡} — in fact, we could have started with such an observationally-closed version of the specification, making no use of observational correctness at this stage yet.

main sort renamed to Set to fit the top level names given in the original requirement specification) will be extended to a component implementing StringHashTable — again, this is to be built via a construction HT′, independently of the details of ASK , for an arbitrary implementation of Array[StringKey]. Finally, the overall result will be given by exporting from this component only the required sorts, operations and predicate.

Notice that the structure here differs in an essential way from the structure of StringHashTable, since we have chosen to forego genericity of hash tables (for arbitrary elements), implementing them for the special case of strings.

Further development might lead to a final implementation in Standard ML, including the following modules. The task of extracting Standard ML signatures (ARRAY_SIG etc., using boolean functions for predicates) from the corresponding Casl signatures of the specifications given above is left for the reader. We assume though that the implementations N of Int and S of String, which we do not spell out here, use the Standard ML built-in types int and string, respectively. These are so-called equality types in Standard ML, and come with the built-in (infix) equality function = which should replace eq_{N} and eq_{S} in the corresponding Standard ML signatures. We also omit a component SK that implements a hash function hash; any total function from strings to integers will do, although of course a good hash function will produce an even distribution of hash values. We compress consecutive instantiations of A' (first to N and then to SK) into a single functor application. Finally, we will incorporate the final adjustment to the overall result signature (the reveal construct in the result unit in StringHashTableDesign) and the renaming of arrays to sets (in the given part of HT) directly into the definition of the functor HT' used to build the resulting hash table of strings.

functor A'(structure N: INT_SIG and E : ELEM_SIG) : ARRAY_SIG =
  struct
    open N E
    type array = int -> elem
    exception unused
    fun empty(i) = raise unused
    fun put(i,e,a)(j) = if i=j then e else a(j)
    fun take(i,a) = a(i)
    fun used(i,a) = (a(i); true) handle unused => false
  end
structure ASK =
  struct
    structure Astring =
       A'(structure N=N and E=struct type elem=SK.string end)
    open Astring
    open SK
  end
functor HT'(structure ASK: ASK_SIG) : STRING_HASH_TABLE_SIG =

  struct
    open ASK
    type set = array
    fun putnear(i,s,t) =
       if used(i,t)
       then if take(i,t)=s then t else putnear(i+1,s,t)
       else put(i,s,t)
    fun add(s,t) = putnear(hash(s),s,t)
    fun isnear(i,s,t) =
       used(i,t) andalso (take(i,t)=s orelse isnear(i+1,s,t))
    fun present(s,t) = isnear(hash(s),s,t)
  end
structure HT = HT'(structure ASK=ASK)

The functor A' is literally correct with respect to Int and Elem and Array[Elem]. To be more precise, the semantic function on the models determined by A' extends any model in [[Int and Elem]] to a model in [[Array[Elem]]] such that [[A']] ∈ [[Int and Elem⟶^{ι}Array[Elem]]], where ι is the obvious signature inclusion. Similarly, the structure HT satisfies the axioms of StringHashTable literally (at least on the reachable part, and assuming the use of extensional equality on functions).

The reader might want to check that StringHashTableDesign is a statically correct architectural specification:^{11} we can derive

⊢ StringHashTableDesign ⊳ ⊳ ((P_{st}, B_{st}), Σ)

where P_{st} binds the generic units declared in StringHashTable (including those implicitly introduced by expanding the given construct for imports), B_{st} maps the non-generic unit names in StringHashTable to their signatures, and Σ is the signature of the result unit (the signature of StringHashTable). Moreover, the (literal) model semantics works as well, so that we have

⊢ StringHashTableDesign ⇒ (C, UEv).

Here, the context C contains all environments that map unit names declared and defined in StringHashTableDesign to their realisations so that declared units satisfy their specifications and the defined units are built from the units given in the environment as prescribed by their respective definitions. Then, the unit evaluator UEv maps any such environment in C to a model as determined by the result unit definition. In particular, the environment determined by the Standard ML functor and structure definitions given above is in C, and UEv maps it to the expected system realisation.

However, even though the above functor A' implementing arrays is correct, we might want to use quite a different array implementation, for instance because it is given as a highly optimised module in a library. Various useful “tricks” in the code then might

11 Using, for instance, the Hets tool, see www.informatik.uni-bremen.de/cofi/hets/.

be expected. Here is an example where each entry in the array includes its history of updates:

functor Atrick(structure N: INT_SIG and E : ELEM_SIG) : ARRAY_SIG =
  struct
    open E
    type array = int -> elem list
    fun empty(i) = nil
    fun put(i,e,a)(j) = if i=j then e::a(j) else a(j)
    fun take(i,a) = let val e::_=a(i) in e end
    fun used(i,a) = not(null a(i))
  end

Then, Atrick given here is not literally correct with respect to Int and Elem and Array[Elem], since it violates the axiom put(i, e′, put(i, e, a)) = put(i, e′, a), but it is observationally correct: [[Atrick]] ∈ [[Int and Elem⟶^{ι}Array[Elem]]]_{≡}. Similarly, the extra flexibility that observational correctness offers would allow us for instance to change the code for HT' to count the number of insertions of each string, yielding a new functor HTtrick'. The structure

structure HTtrick = HTtrick'(structure ASK=ASK)

violates the axiom used(i, a) ∧ take(i, a) = s ⟹ putnear(i, s, a) = a, but again it is observationally correct: [[HTtrick]] ∈ [[StringHashTable]]_{≡}.

The unit environment determined by Atrick' and HTtrick' is not in the context C given by the literal model semantics of StringHashTable. However, under the observational semantics, we have:

⊢ StringHashTableDesign ⟹^{≡} (C_{♭}, UEv_{♭}),

where C_{♭} contains the environment that is determined by Atrick' and HTtrick'. Moreover, UEv_{♭} (which essentially coincides with UEv given by the literal model semantics above, but works on a different domain) maps such an environment to a model of the whole system that is an observationally correct realisation of the original specification StringHashTable, as expected.

The Standard ML functors above define locally stable constructions: they respect encapsulation since they do not use any properties of their arguments other than what is spelled out in their parameter signatures. Indeed, all closed functors (which do not refer to external structure definitions) in Standard ML define locally stable constructions.

Let us now go back to the idea inherent in the structure of the specification StringHashTable, and try to build our implementation using a generic construction for hash tables. That structure may be captured by the following architectural specification:

arch spec StringHashTableDesign′ =

units N : Int; A : Elem → Array[Elem] given N; HT_{gen} : ElemKey × Array[Elem] → HashTable[ElemKey]; S : String; SK : StringKey given S, N;

result HT_{gen}[SK fit Elem ↦ String][A[S]] with Array[String] ↦ Set reveal String, Set, empty, add, present

This is a correct architectural specification again, and indeed we get:

⊢ StringHashTableDesign′ ⊳ ⊳ ((P′_{st}, B′_{st}), Σ) ⊢ StringHashTableDesign′ ⇒ (C′, UEv′) ⊢ StringHashTableDesign′ ⟹^{≡} (C′_{♭}, UEv′_{♭})

The extended static semantics and the literal model semantics work as expected (we encourage the reader to try to describe the resulting contexts). However, perhaps unexpectedly, we get C′_{♭} = ∅ — the above architectural specification is observationally inconsistent! The trouble is, of course, with the specification of generic hash tables. One might try to implement it as follows:

functor HTgen
    (structure EK : ELEM_KEY_SIG and A : ARRAY_ELEM_KEY_SIG
         sharing type EK.elem=A.elem) : HASH_TABLE_ELEM_KEY_SIG =
  struct
    open EK A
    fun putnear(i,e,a) =
       if used(i,a)
       then if take(i,a)=e then a else putnear(i+1,e,a)
       else put(i,e,a)
    fun add(e,a) = putnear(hash(e),e,a)
    fun isnear(i,e,a) =
       used(i,a) andalso (take(i,a)=e orelse isnear(i+1,e,a))
    fun present(e,a) = isnear(hash(e),e,a)
  end

Unfortunately, the construction defined by HTgen is not locally stable, and in fact HTgen is not correct code in Standard ML, since it requires equality on elem (in take(i,a)=e) which is not provided by ELEM_KEY_SIG. This problem is not accidental: there is no locally stable construction, and hence no Standard ML functor, satisfying the required specification. Consequently, there are no stable environments in context C′ resulting from the literal model semantics — hence the observational inconsistency of StringHashTableDesign′ (C′_{♭} = ∅). Even though what is a reasonable structure for the requirements specification, as expressed in StringHashTable, led to an inappropriate modular design StringHashTableDesign′, this is in fact good news. While allowing for a more relaxed interpretation of the axioms in (result) specifications as long as their observable consequences are ensured, the observational semantics marked as inconsistent a specification that cannot be implemented in a reasonable programming language in which no tricky means are available to violate the modular structure.

Of course, this does not mean that there is no good design that would require a generic implementation of hash tables. A simple way to achieve this would be to modify the above architectural specification to add “equality” on Elem by introducing an equality predicate (for instance, in ElemKey). Notice that this is different from requiring Elem to be an equality type as in Standard ML, since this predicate is not necessarily constrained to be interpreted as the identity. Consequently, we should then use this predicate, rather than identity, to compare elements stored in HashTable. One point of architectural specifications is that such change of structure is an important design decision that deserves to be recorded explicitly. The new specifications would be as follows:

spec ElemKeyEq = Elem and Int then op hash : Elem → Int;

pred eq_{E} : Elem × Elem

spec HashTableEq[ElemKeyEq] = ElemKeyEq and Array[Elem]

then ops add : Elem × Array[Elem] → Array[Elem];

putnear : Int × Elem × Array[Elem] → Array[Elem] preds present : Elem × Array[Elem]

isnear : Int × Elem × Array[Elem] ∀ i : Int; e : Elem; a : Array[Elem]

• add(e, a) = putnear(hash(e), e, a)

• ¬used(i, a) ⟹ putnear(i, e, a) = put(i, e, a)

• used(i, a) ∧ eq_{E}(take(i, a), e) ⟹ putnear(i, e, a) = a • used(i, a) ∧ ¬eq_{E}(take(i, a), e) ⟹ putnear(i, e, a) = putnear(succ(i), e, a)

• present(e, a) ⟺ isnear(hash(e), e, a)

• ¬used(i, a) ⟹ ¬isnear(i, e, a)

• used(i, a) ∧ eq_{E}(take(i, a), e) ⟹ isnear(i, e, a)

• used(i, a) ∧ ¬eq_{E}(take(i, a), e) ⟹ (isnear(i, e, a) ⟺ isnear(succ(i), e, a))

The architectural design then might look as follows:

arch spec StringHashTableDesignEq =

units N : Int; A : Elem → Array[Elem] given N; HT_{gen} : ElemKeyEq × Array[Elem] → HashTableEq[ElemKeyEq]; S : String; SK : StringKey given S, N;

result HT_{gen}[SK fit Elem ↦ String][A[S]] with Array[String] ↦ Set

reveal String, Set, empty, add, present

The following Standard ML functor would then provide a generic implementation of hash tables for any type of elements with an equality function, yielding a locally stable construction that is (observationally) correct with respect to ElemKeyEq and Array[Elem] and HashTableEq[ElemKeyEq]:

functor HTEQgen
    (structure EK : ELEM_KEY_EQ_SIG and A : ARRAY_ELEM_KEY_SIG

         sharing type EK.elem=A.elem) : HASH_TABLE_ELEM_KEY_EQ_SIG =
  struct
    open EK A
    fun putnear(i,e,a) =
       if used(i,a)
       then if eq_E(take(i,a),e) then a else putnear(i+1,e,a)
       else put(i,e,a)
    fun add(e,a) = putnear(hash(e),e,a)
    fun isnear(i,e,a) =
       used(i,a) andalso (eq_E(take(i,a),e) orelse isnear(i+1,e,a))
    fun present(e,a) = isnear(hash(e),e,a)
  end

9. Conclusions and Further Work

The overall goal of this paper is to provide an observational view of Casl specifications that supports observational refinement of specifications in combination with Casl-style architectural design. This is achieved, and spelled out in detail for a simplified version of Casl architectural specifications. Extending this to full Casl architectural specifications (by allowing multiple parameters for parametrized units, adding unit translations, etc.) is straightforward. Imports of units defined by arbitrary unit expressions are the only potential source of difficulty. But the methodologically well-justified case of this, where the import can be given an explicit specification, is easily dealt with as in Sect. 8.

Although we have worked in the specific setting of Casl signatures and models, formulated as an institution in Sect. 2, it should be clear that much of the above applies to a wide range of institutions. Rather than attempting to spell out the appropriate notion of “institution with extra structure”, let us just remark that surprisingly little appears to be required. A notion of observational model morphisms that is closed under composition and reduct, plus some extra categorical structure to identify “correspondences” as certain spans of such morphisms, seems necessary and sufficient to formulate most of the material presented. The need for additional structure is obviated by the fact that the technical development makes no reference to a set of observable sorts, in contrast to standard approaches to observational interpretation of specifications. In the context of Casl (where one can treat a sort as observable by introducing an “equality predicate” on it) this is adequate. It may well not be adequate in institutions of much more limited expressive power, but it is not clear that such institutions are of genuine practical importance. Links with indistinguishability relations via factorization properties, like Thm. 5.8, may require the richer context of concrete institutions, where model categories are equipped with concretization structure subject to a number of technical requirements as in (Bidoit and Tarlecki 1996), or alternatively may follow the ideas of (Popescu and Roşu 2005).

A challenging issue is now to understand how far the concepts developed for our somewhat simplified view of software components as local constructions on Casl models can be inspiring for a more general view of components involving some form of external communication. While this is clearly beyond the scope of this paper, we nevertheless imagine that a promising direction of future research would be to look for an adequate counterpart of (local) stability in this more general setting.

Acknowledgements. Our thanks to the CoFI Language Design and Semantics Task Groups for many discussions and opportunities to present and improve our ideas on architectural specifications, and thanks in particular to Piotr Hoffman, Bartek Klin, Till Mossakowski and Lutz Schröder for collaboration on their semantics. Thanks also to one of the anonymous reviewers for careful checking and perceptive comments. This work has been partially supported by European projects IST-2001-32747 AGILE (AT), IST-2005-015905 MOBIUS (DS, AT) and IST-2005-016004 SENSORIA (AT), the EPSRC-funded ReQueST project (DS), the British–Polish Research Partnership Programme (DS, AT), and Visiting Professorships at ENS de Cachan (AT).

References

E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Brückner, P.D. Mosses, D. Sannella and A. Tarlecki. Casl: The Common Algebraic Specification Language. Theoretical Computer Science 286:153–196 (2002).

E. Astesiano, B. Krieg-Brückner and H.-J. Kreowski, eds. Algebraic Foundations of Systems

Specification. Springer (1999). H. Baumeister, M. Cerioli, A. Haxthausen, T. Mossakowski, P.D. Mosses, D. Sannella and A.

Tarlecki. Casl Semantics. In: (Mosses 2004), 115–273. G. Bernot. Good functors … are those preserving philosophy! Proc. 2nd Summer Conf. on

Category Theory and Computer Science CTCS’87, Springer LNCS 283, 182–195 (1987). M. Bidoit and R. Hennicker. A general framework for modular implementations of modular

systems. Proc. 4th Int. Conf. on Theory and Practice of Software Development TAPSOFT’93, Springer LNCS 668, 199–214 (1993).

M. Bidoit and R. Hennicker. Modular correctness proofs of behavioural implementations. Acta

Informatica 35(11):951–1005 (1998). M. Bidoit and R. Hennicker. Proving behavioral refinements of COL-specifications. Algebra,

Meaning and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday. Springer LNCS 4060, 333–354 (2006).

M. Bidoit, R. Hennicker and M. Wirsing. Behavioural and abstractor specifications. Science of

Computer Programming 25:149–186 (1995). M. Bidoit and P.D. Mosses. Casl User Manual. Springer LNCS 2900 (IFIP Series), 2004. M. Bidoit, D. Sannella and A. Tarlecki. Architectural specifications in Casl. Formal Aspects of

Computing, 13:252–273 (2002a). M. Bidoit, D. Sannella and A. Tarlecki. Global development via local observational construction

steps. Proc. 27th Intl. Symp. on Mathematical Foundations of Computer Science, MFCS’02. Springer LNCS 2420, 1–24 (2002b).

M. Bidoit, D. Sannella and A. Tarlecki. Toward component-oriented formal software development: an algebraic approach. Proc. 9th Monterey Workshop, Radical Innovations of Software and Systems Engineering in the Future, Venice, October 2002. Springer LNCS 2941, 75–90 (2004).

M. Bidoit and A. Tarlecki. Behavioural satisfaction and equivalence in concrete model categories. Proc. 20th Coll. on Trees in Algebra and Computing CAAP’96, Linköping, Springer LNCS 1059, 241–256 (1996).

Observational Interpretation of Casl Specifications 45

P. Burmeister. A Model Theoretic Approach to Partial Algebras. Akademie Verlag, Berlin (1986). R. Burstall and J. Goguen. The semantics of Clear, a specification language. Proc. Advanced

Course on Abstract Software Specifications, Copenhagen. Springer LNCS 86, 292–332 (1980). The CoFI Language Design Group. Casl Summary. B. Krieg-Brückner and P.D. Mosses, eds.

In: (Mosses 2004), 3–74. H. Ehrig and H.-J. Kreowski. Refinement and implementation. In: (Astesiano, Krieg-Brückner

and Kreowski 1999), 201–242. H. Ehrig, H.-J. Kreowski, B. Mahr and P. Padawitz. Algebraic implementation of abstract data

types. Theoretical Computer Science 20:209–263 (1982). H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification I: Equations and Initial Seman-

tics. Springer (1985). H. Ganzinger. Parameterized specifications: parameter passing and implementation with re-

spect to observability. ACM Transactions on Programming Languages and Systems 5:318–354 (1983).

V. Giarratana, F. Gimona and U. Montanari. Observability concepts in abstract data type specifications. Proc. 5th Intl. Symp. on Mathematical Foundations of Computer Science, Springer LNCS 45, 576–587 (1976).

A. Ginzburg. Algebraic Theory of Automata. Academic Press (1968). J. Goguen and R. Burstall. Institutions: abstract model theory for specification and program-

ming. Journal of the ACM 39:95–146 (1992). J. Goguen, J. Thatcher and E. Wagner. An initial algebra approach to the specification, correct-

ness and implementation of abstract data types. Current Trends in Programming Methodology, Vol. 4: Data Structuring (R.T. Yeh, ed.). Prentice-Hall, 80–149 (1978).

J. Guttag and J. Horning. Larch: Languages and Tools for Formal Specification. Springer (1993). C.A.R. Hoare. Proofs of correctness of data representations. Acta Informatica 1:271–281 (1972). P. Hoffman. Verifying architectural specifications. Recent Trends in Algebraic Development Tech-

niques, Selected Papers, WADT’01, Springer LNCS 2267, 152-175 (2001). F. Honsell, J. Longley, D. Sannella and A. Tarlecki. Constructive data refinement in typed

lambda calculus. Proc. 2nd Intl. Conf. on Foundations of Software Science and Computation Structures. Springer LNCS 1784, 149–164 (2000).

S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML: a gentle introduction.

Theoretical Comp. Sci. 173:445–484 (1997). B. Klin, P. Hoffman, A. Tarlecki, L. Schröder and T. Mossakowski. Checking amalgamability

conditions for Casl architectural specifications. Proc. 26th Intl. Symp. Mathematical Foundations of Computer Science MFCS’01, Springer LNCS 2136, 451–463 (2001).

R. Milner. An algebraic definition of simulation between programs. Proc. 2nd Intl. Joint Conf.

on Artificial Intelligence, London, 481–489 (1971). T. Mossakowski, P. Hoffman, S. Autexier and D. Hutter. Casl Logic. In: (Mosses 2004), 275–359. P.D. Mosses, ed. Casl Reference Manual. Springer LNCS 2960 (IFIP Series), 2004. A. Popescu and G. Roşu. Behavioral extensions of institutions. Proc. 1st Conf. on Algebra and

Coalgebra in Computer Science CALCO’05, Swansea. Springer LNCS 3629, 331–347 (2005). H. Reichel. Behavioural equivalence — a unifying concept for initial and final specification

methods. Proc. 3rd Hungarian Comp. Sci. Conference, 27–39 (1981). D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Com-

putation 76:165–210 (1988a). D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifica-

tions: implementations revisited. Acta Informatica 25:233–281 (1988b).

D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Proc. Colloq. on Current Issues in Programming Languages, Intl. Joint Conf. on Theory and Practice of Software Development TAPSOFT’89, Barcelona. Springer LNCS 352, 375–389 (1989).

D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program develop-

ment. Formal Aspects of Computing 9:229–269 (1997). O. Schoett. Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis, report

CST-42-87, Dept. of Computer Science, Univ. of Edinburgh (1987). O. Schoett. Behavioural correctness of data representations. Science of Computer Programming

14:43–57 (1990). L. Schröder and T. Mossakowski. HasCasl: Towards integrated specification and development of

functional programs. Proc. 9th Intl. Conf. on Algebraic Methodology and Software Technology, AMAST’02. Springer LNCS 2422, 99–116 (2002).

L. Schröder, T. Mossakowski, A. Tarlecki, P. Hoffman and B. Klin. Semantics of architectural specifications in Casl. Proc. 4th Intl. Conf. Fundamental Approaches to Software Engineering FASE’01, Springer LNCS 2029, 253–268 (2001).

L. Schröder, T. Mossakowski, A. Tarlecki, P. Hoffman and B. Klin. Amalgamation in the se-

mantics of Casl. Theoretical Computer Science, 331:215–247 (2005). C. Szyperski. Component Software: Beyond Object-Oriented Programming. ACM Press and

Addison-Wesley, New-York, N.Y. (1998). A. Tarlecki. Abstract specification theory: An overview. In Models, Algebras and Logic of Engi-

neering Software, M. Broy and M. Pizka, eds., NATO Science Series - Computer and Systems Sciences, Vol. 191, 43–79, IOS Press, 2003.