Computing and Informatics, Vol. 20, 2001, ??–??, V 2003-Sep-4

Casl — THE COMMON ALGEBRAIC SPECIFICATION LANGUAGE: SEMANTICS AND PROOF THEORY

Till Mossakowski

Department of Computer Science, University of Bremen, Germany

e-mail: till@tzi.de

Anne Haxthausen

Informatics and Mathematical Modelling, Techn. University of Denmark, Lyngby

e-mail: ah@imm.dtu.dk

Donald Sannella

LFCS, School of Informatics, University of Edinburgh, Edinburgh, UK

e-mail: dts@inf.ed.ac.uk

Andrzej Tarlecki

Institute of Informatics, Warsaw University and Institute of Computer Science, PAS, Warsaw, Poland

e-mail: tarlecki@mimuw.edu.pl

Abstract. Casl is an expressive specification language that has been designed to supersede many existing algebraic specification languages and provide a standard. Casl consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications (the latter are used to prescribe the structure of implementations).

We describe an simplified version of the Casl syntax, semantics and proof calculus at each of these three layers and state the corresponding soundness and completeness theorems. The layers are orthogonal in the sense that the semantics of a given layer uses that of the previous layer as a “black box”, and similarly for the proof calculi. In particular, this means that Casl can easily be adapted to other logical systems.

Keywords: Algebraic specification, formal software development, logic, calculi, institutions

1 INTRODUCTION

Algebraic specification is one of the most extensively-developed approaches in the formal methods area. The most fundamental assumption underlying algebraic specification is that programs are modelled as algebraic structures that include a collection of sets of data values together with functions over those sets. This level of abstraction is commensurate with the view that the correctness of the input/output behaviour of a program takes precedence over all its other properties. Another common element is that specifications of programs consist mainly of logical axioms, usually in a logical system in which equality has a prominent role, describing the properties that the functions are required to satisfy—often just by their interrelationship. This property-oriented approach is in contrast to so-called model-oriented specifications in frameworks like VDM [24] which consist of a simple realization of the required behaviour. However, the theoretical basis of algebraic specification is largely in terms of constructions on algebraic models, so it is at the same time much more model-oriented than approaches such as those based on type theory (see e.g. [41]), where the emphasis is almost entirely on syntax and formal systems of rules, and semantic models are absent or regarded as of secondary importance.

Casl [4] is an expressive specification language that has been designed by CoFI, the international Common Framework Initiative for algebraic specification and development [38, 16], with the goal to subsume many previous algebraic specification languages and to provide a standard language for the specification and development of modular software systems.

This paper gives an overview of the semantic concepts and proof calculi underlying Casl. Section 2 starts with institutions and logics, abstract formalizations of the notion of logical system. The remaining sections follow the layers of the Casl language:

1. Basic specifications provide the means to write specifications in a particular institution, and providing a proof calculus for reasoning within such unstructured specifications. The institution underlying Casl, together with its proof calculus, is presented in Sections 3 (for many-sorted basic specifications) and 4 (the extension to subsorting). Section 5 explains some of the language constructs that allow one to write down theories in this institution rather concisely.

Casl — The Common Algebraic Specification Language: semantics and proof theory 3

2. Structured specifications, expressing how more complex specifications are built from simpler ones (Section 6). The semantics and proof calculus is given in a way that is parameterized over the particular institution and proof calculus for basic specifications (as given at the basic specification layer). Hence, the institution and proof calculus for basic specifications can be changed without the need to change anything for structured specifications.

3. Architectural specifications, in contrast to structured specifications, prescribe the structure of the implementation, with the possibility of enforcing a separate development of composable, reusable implementation units (Section 7). Again, the semantics and proof calculus at this layer is formulated in terms of the semantics and proof calculus given in the previous layers.

4. Finally, libraries of specifications allow the (distributed) storage and retrieval of named specifications. Since this is rather straightforward, space considerations led to the omission of this layer of Casl in the present work.

Due to space limitations, this paper only covers a simplified version of Casl, and mainly introduces semantic concepts, while language constructs are only briefly treated in Section 5. A full account of Casl (also covering libraries of specifications) will appear in [40] (see also [16, 4, 34]), while a gentle introduction is provided in [39].

2 INSTITUTIONS AND LOGICS

First, before considering the particular concepts underlying Casl, we recall how specification frameworks in general may be formalized in terms of so-called institutions [19].

An institution I = (Sign, Sen, Mod, ⊧) consists of

• a category Sign of signatures,

• a functor Sen: Sign → Set giving, for each signature Σ, a set of sentences Sen(Σ), and for each signature morphism σ: Σ → Σ′, a sentence translation map Sen(σ): Sen(Σ)→Sen(Σ′), where Sen(σ)(φ) is often written σ(φ),

• a functor Mod: Sign^{op} → CAT ^{1} giving, for each signature Σ, a category of models Mod(Σ), and for each signature morphism σ: Σ → Σ′, a reduct functor Mod(σ): Mod(Σ′)→Mod(Σ), where Mod(σ)(M′) is often written M′|_{σ},

• a satisfaction relation ⊧_{Σ} ⊆ |Mod(Σ)| × Sen(Σ) for each Σ ∈ Sign,

such that for each σ: Σ→Σ′ in Sign the following satisfaction condition holds:

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

1 Here, CAT is the quasi-category of all categories. As metatheory, we use ZF CU, i.e.

ZF with axiom of choice and a set-theoretic universe U. This allows for the construction of quasi-categories, i.e. categories with more than a class of objects. See [22].

for each M′ ∈ Mod(Σ′) and φ ∈ Sen(Σ).

An institution with unions is an institution equipped with a partial binary operation ∪ on signatures, such that there are two “inclusions” ι_{1} : Σ_{1} → Σ_{1} ∪ Σ_{2} and ι_{2} : Σ_{2} → Σ_{1} ∪ Σ_{2}. We write M|_{Σ_{i}} for M|_{ι_{i}: Σ_{i}→Σ_{1}∪Σ_{2}} (i = 1, 2) whenever ι_{i} is clear from the context. Typically (e.g. in the Casl institution), ∪ is a total operation. However, in institutions without overloading, generally two signatures giving the same name to different things cannot be united.

Further properties of signature unions, as well as other requirements on institutions, are needed only in Sect. 7 on architectural specifications and will be introduced there.

Within an arbitrary but fixed institution, we can easily define the usual notion of logical consequence or semantical entailment. Given a set of Σ-sentences Γ and a Σ-sentence φ, we say that φ follows from Γ, written Γ ⊧_{Σ} φ, iff for all Σ-models M, we have M ⊧_{Σ} Γ implies M ⊧_{Σ} φ. (Here, M ⊧_{Σ} Γ means that M ⊧_{Σ} ψ for each ψ ∈ Γ.)

Coming to proofs, a logic [29] extends an institution with proof-theoretic entailment relations that are compatible with semantic entailment.

A logic LOG = (Sign, Sen, Mod, ⊧, ⊢) is an institution (Sign, Sen, Mod, ⊧) equipped with an entailment system ⊢, that is, a relation ⊢_{Σ} ⊆ P(Sen(Σ))×Sen(Σ) for each Σ ∈ |Sign|, such that the following properties are satisfied:

1. reflexivity: for any φ ∈ Sen(Σ), {φ} ⊢_{Σ} φ,

2. monotonicity: if Γ ⊢_{Σ} φ and Γ′ ⊇ Γ then Γ′ ⊢_{Σ} φ,

3. transitivity: if Γ ⊢_{Σ} φ_{i} for i ∈ I and Γ ∪ {φ_{i} | i ∈ I} ⊢_{Σ} ψ, then Γ ⊢_{Σ} ψ,

4. ⊢-translation: if Γ ⊢_{Σ} φ, then for any σ: Σ→Σ′ in Sign, σ(Γ) ⊢_{Σ′} σ(φ),

5. soundness: if Γ ⊢_{Σ} φ then Γ ⊧_{Σ} φ.

A logic is complete if, in addition, Γ ⊧_{Σ} φ implies Γ ⊢_{Σ} φ.

It is easy to obtain a complete logic from an institution by simply defining ⊢ as ⊧. Hence, ⊢ might appear to be redundant. However, the point is that ⊢ will typically be defined via a system of finitary derivation rules. This gives rise to a notion of proof that is absent when the institution is considered on its own, even if the relation that results coincides with semantic entailment which is defined in terms of the satisfaction relation.

3 MANY-SORTED BASIC SPECIFICATIONS

Casl’s basic specification layer is an expressive language that integrates subsorts, partiality, first-order logic and induction (the latter expressed using so-called sort generation constraints).

3.1 Many-sorted institution

The institution underlying Casl is introduced in two steps [8, 14]. In this section, we introduce the institution of many-sorted partial first-order logic with sort generation constraints and equality, P CF OL^{=}. In Section 4, subsorting is added.

3.1.1 Signatures

A many-sorted signature Σ = (S, TF , PF , P) consists of a set S of sorts, S^{∗}×Sindexed families TF and PF of total and partial function symbols, with TF_{w,s} ∩ PF_{w,s} = ∅ for each (w, s) ∈ S^{∗}×S, where constants are treated as functions with no arguments, and an S^{∗}-indexed family P of predicate symbols. We write f : w → s ∈ TF for f ∈ TF_{w,s} (with f : s for empty w), f : w →? s ∈ PF for f ∈ PF_{w,s} (with f :→? s for empty w) and p : w ∈ P for p ∈ P_{w}.

Although TF_{w,s} and PF_{w,s} are required to be disjoint, so that a function symbol with a given profile cannot be both partial and total, function and predicate symbols may be overloaded: we do not require e.g. TF_{w,s} and TF_{w′,s′} (or TF_{w,s} and PF_{w′,s′} ) to be disjoint for (w, s) ≠ (w′, s′). To ensure that there is no ambiguity in sentences, however, symbols are always qualified by profiles when used. In the Casl language constructs (see Section 5), such qualifications may be omitted when they are unambiguously determined by the context.

Given signatures Σ and Σ′, a signature morphism σ: Σ→Σ′ maps sorts, function symbols and predicate symbols in Σ to symbols of the same kind in Σ′. A partial function symbol may be mapped to a total function symbol, but not vice versa, and profiles must be preserved, so for instance f : w → s in Σ maps to a function symbol in Σ′ with profile σ^{∗}(w) → σ(s), where σ^{∗} is the extension of σ to finite strings of symbols. Identities and composition are defined in the obvious way, giving a category Sign of P CF OL^{=}-signatures.

3.1.2 Models

Given a finite string w = s_{1} … s_{n} and sets M_{s_{1}}, …, M_{s_{n}}, we write M_{w} for the Cartesian product M_{s_{1}} × ⋯ × M_{s_{n}}. Let Σ = (S, TF , PF , P).

A many-sorted Σ-model M consists of a non-empty carrier set M_{s} for each sort s ∈ S, a total function (f_{w,s})_{M} : M_{w} → M_{s} for each total function symbol f : w → s ∈ TF , a partial function (f_{w,s})_{M} : M_{w} ⇀ M_{s} for each partial function symbol f : w →? s ∈ PF , and a predicate (p_{w})_{M} ⊆ M_{w} for each predicate symbol p : w ∈ P. Requiring carriers to be non-empty simplifies deduction and makes it unproblematic to regard axioms (see Section 3.1.3) as implicitly universally quantified. A slight drawback is that the existence of initial models is lost in some cases, even if only equational axioms are used, namely if the signature is such that there are no ground terms of some sort. However, from a methodological point of view, specifications with such signatures typically are used in a context where loose rather than initial semantics is appropriate.

A many-sorted Σ-homomorphism h : M → N maps the values in the carriers of M to values in the corresponding carriers of N in such a way that the values of functions and their definedness is preserved, as well as the truth of predicates. Identities and composition are defined in the obvious way. This gives a category Mod(Σ).

Concerning reducts, if σ: Σ→Σ′ is a signature morphism and M′ is a Σ′-model, then M′|_{σ} is a Σ-model with (M′|_{σ})_{s} := M′_{σ(s)} for s ∈ S and analogously for (f_{w,s})_{M′|_{σ}} and (p_{w})_{M′|_{σ}}. The same applies to any Σ′-homomorphism h′: M′ → N′: its reduct h′|_{σ}: M′|_{σ} → N′|_{σ} is the Σ-homomorphism defined by (h′|_{σ})_{s} := h′_{σ(s)} for s ∈ S. It is easy to see that reduct preserves identities and composition, so we obtain a functor Mod(σ): Mod(Σ′)→Mod(Σ). Moreover, it is easy to see that reducts are compositional, i.e., we have, for example, (M′′|_{θ})|_{σ} = M′′|_{σ;θ} for signature morphisms σ: Σ→Σ′, θ: Σ′ →Σ′′ and Σ′′-models M′′. This means that we have indeed defined a functor Mod: Sign^{op} →CAT .

3.1.3 Sentences

Let Σ = (S, TF , PF , P). A variable system over Σ is an S-sorted, pairwise disjoint family of variables X = (X_{s})_{s∈S}. Let such a variable system be given.

As usual, the many-sorted Σ-terms over X are defined inductively as comprising the variables in X, which have uniquely-determined sorts, together with applications of function symbols to argument terms of appropriate sorts, where the sort is determined by the profile of its outermost function symbol. This gives an S-indexed family of sets T_{Σ}(X) which can be made into a (total) many-sorted Σ-model by defining (f_{w,s})_{T_{Σ}(X)} to be the term-formation operations for f : w → s ∈ TF and f : w →? s ∈ PF , and (p_{w})_{T_{Σ}(X)} = ∅ for p : w ∈ P.

An atomic Σ-formula is either: an application p_{w}(t_{1}, …, t_{n}) of a predicate symbol to terms of appropriate sorts; an existential equation t =^{e} t′ or strong equation t =^{s} t′ between two terms of the same sort; or an assertion def t that the value of a term is defined. This defines the set AF_{Σ}(X) of many-sorted atomic Σ-formulas with variables in X. The set F O_{Σ}(X) of many-sorted first-order Σ-formulas with variables in X is then defined by adding a formula F (false) and closing under conjunction φ ∧ ψ, implication φ ⇒ ψ and universal quantification ∀x : s • φ. We use the usual abbreviations: ¬φ for φ ⇒ F, φ ∨ ψ for ¬(¬φ ∧ ¬ψ), T for ¬F and ∃x : s • φ for ¬∀x : s • ¬φ.

A sort generation constraint states that a given set of sorts is generated by a given set of functions. Technically, sort generation constraints also contain a signature morphism component; this allows them to be translated along signature morphisms without sacrificing the satisfaction condition. Formally, a sort generation constraint over a signature Σ is a triple (S̃, F̃, θ), where θ: \overline{Σ} → Σ, \overline{Σ} = (\overline{S}, \overline{TF} , \overline{PF} , \overline{P}), S̃ ⊆ \overline{S} and F̃ ⊆ \overline{TF} ∪ \overline{PF} .

Now a Σ-sentence is either a closed many-sorted first-order Σ-formula (i.e. a many-sorted first-order Σ-formula over the empty set of variables), or a sort generation constraint over Σ.

Given a signature morphism σ: Σ → Σ′ and variable system X over Σ, we can get a variable system σ(X) over Σ′ by taking

σ(X)_{s′} := ⋃_{σ(s)=s′} X_{s}

Since T_{Σ}(X) is total, the inclusion ζ_{σ,X}: X → T_{Σ′}(σ(X))|_{σ} (regarded as a variable valuation) leads to a term evaluation function

ζ_{σ,X}^{#} : T_{Σ}(X)→T_{Σ′}(σ(X))|_{σ}

that is total as well. This can be inductively extended to a translation along σ of Σfirst order formulas with variables in X by taking σ(t) := ζ_{σ,X}^{#}(t), σ(p_{w}(t_{1}, …, t_{n})) :=

σ_{w}(p)_{σ^{∗}(w)}(σ(t_{1}), …, σ(t_{n})), σ(t =^{e} t′) := σ(t) =^{e} σ(t′), σ(∀x : s • φ) = ∀x :

σ(s) • σ(φ), and so on. The translation of a Σ-constraint (S̃, F̃, θ) along σ is the Σ′- constraint (S̃, F̃, θ;σ). It is easy to see that sentence translation preserves identities and composition, so sentence translation is functorial.

3.1.4 Satisfaction

Variable valuations are total, but the value of a term with respect to a variable valuation may be undefined, due to the application of a partial function during the evaluation of the term. Given a variable valuation ν: X → M for X in M, term evaluation ν^{#} : T_{Σ}(X) ⇀ M is defined in the obvious way, with t ∈ dom(ν^{#}) iff all partial functions in t are applied to values in their domains.

Even though the evaluation of a term with respect to a variable valuation may be undefined, the satisfaction of a formula φ in a model M is always defined, and it is either true or false: that is, we have a two-valued logic. The application p_{w}(t_{1}, …, t_{n}) of a predicate symbol to a sequence of argument terms is satisfied with respect to a valuation ν: X → M iff the values of all of t_{1}, …, t_{n} are defined under ν^{#} and give a tuple belonging to p_{M}. A definedness assertion def t is satisfied iff the value of t is defined. An existential equation t_{1} =^{e} t_{2} is satisfied iff the values of t_{1} and t_{2} are defined and equal, whereas a strong equation t_{1} =^{s} t_{2} is also satisfied when the values of both t_{1} and t_{2} are undefined; thus both notions of equation coincide for defined terms. Satisfaction of other formulae is defined in the obvious way. A formula φ is satisfied in a model M, written M ⊧ φ, iff it is satisfied with respect to all variable valuations into M.

A Σ-constraint (S̃, F̃, θ) is satisfied in a Σ-model M iff the carriers of M|_{θ} of sorts in S̃ are generated by the function symbols in F̃, i.e. for every sort s ∈ S̃ and every value a ∈ (M|_{θ})_{s}, there is a \overline{Σ}-term t containing only function symbols from F̃ and variables of sorts not in S̃ such that ν^{#}(t) = a for some valuation ν into M|_{θ}.

For a sort generation constraint (S̃, F̃, θ) we can assume without loss of generality that all the result sorts of function symbols in F̃ occur in S̃. If not, we can just omit from F̃ those function symbols not satisfying this requirement, without affecting satisfaction of the sort generation constraint: in the \overline{Σ}-term t witnessing the satisfaction of the constraint, any application of a function symbol with result sort outside S̃ can be replaced by a variable of that sort, which gets as assigned value the evaluation of the function application.

For a proof of the satisfaction condition, see [34].

3.2 Proof calculus

We now come to the proof calculus for Casl many-sorted basic specification. The rules of derivation are given in Fig. 1.

The first rules (up to ∀-intro) are standard rules of first-order logic [7]. Reflexivity, Congruence and Substitution differ from the standard rules since they have to take into account potential undefinedness of terms. Hence, Reflexivity only holds for variables (which by definition are always defined), and Substitution needs the assumption that the terms being substituted are defined. (Note that definedness, D(t), is just an abbreviation for the existential equality t =^{e} t.) Totality, Function Strictness and Predicate Strictness have self-explanatory names; they allow to infer definedness statements. Finally, the last two rules deal with sort generation constraints. If these are seen as second-order universally quantified formulas, Induction corresponds to second-order ∀-Elim, and Sortgen-Intro corresponds to second-order ∀-Intro. The φ_{j} correspond to the inductive bases and inductive steps that have to be shown, while the formula ⋀_{s∈S} ∀x : θ(s) • Ψ_{s}(x) is the statement that is shown by induction (note that if S consists of more than one sort, we have a parallel induction running simultaneously over several sorts).

A derivation of Φ ⊢ φ is a tree (called derivation tree) such that

• the root of the tree is φ,

• all the leaves of the tree are either in Φ or marked as local assumption,

• each non-leaf node is an instance of the conclusion of some rule, with its children being the correspondingly instantiated premises,

• any assumptions marked with […] in the proof rules are marked as local assumptions.

If Φ and φ consist of Σ-formulas, we also write Φ ⊢_{Σ} φ. In practice, one will work with acyclic graphs instead of trees, since this allows the re-use of lemmas.

Some rules contain a condition that some variables occur freely only in local assumptions. These conditions are the usual Eigenvariable conditions of natural deduction style calculi. They more precisely mean that if the specified variables occur freely in an assumption in a proof tree, the assumption must be marked as local and have been used in the proof of the premise of the respective rule.

The following theorem is proved in [37]:

Theorem 1. The above proof calculus yields an entailment system. Equipped with this entailment system, the Casl institution SubP CF OL^{=} becomes a sound logic. Moreover, it is complete if sort generation constraints are not used.

(Absurdity) \frac{false}{φ}  (Tertium non datur) \frac{\begin{matrix}[φ] & [φ ⇒ false] \\ ⋮ & ⋮ \\ ψ & ψ \end{matrix}}{ψ}

(⇒-intro) \frac{[φ] ; ⋮ ; ψ}{φ ⇒ ψ}  (⇒-elim) \frac{\begin{matrix}φ \\ φ ⇒ ψ \end{matrix}}{ψ}  (∀-elim) \frac{∀x : s.φ}{φ}
(∀-intro) \frac{φ}{∀x : s.φ} where x_{s} occurs freely only in local assumptions
(Reflexivity) \overline{x_{s} =^{e} x_{s}} if x_{s} is a variable

(Congruence) \frac{φ}{(⋀_{x_{s}∈F V (φ)} x_{s} =^{e} ν(x_{s})) ⇒ φ[ν]} if φ[ν] defined

(Substitution) \frac{φ}{(⋀_{x_{s}∈F V (φ)} D(ν(x_{s}))) ⇒ φ[ν]}

if φ[ν] defined and F V (φ) occur freely only in local assumptions

(Totality) \overline{D(f_{w,s}⟨x_{s_{1}}, …, x_{s_{n}}⟩)} if w = s_{1} … s_{n}, f ∈ T F_{w,s}

(Function Strictness) \frac{t_{1} =^{e} t_{2}}{D(t)} t some subterm of t_{1} or t_{2}

(Predicate Strictness) \frac{p_{w}⟨t_{1}, …, t_{n}⟩}{D(t_{i})} i ∈ \{1, …, n\}

(Induction) \frac{\begin{matrix}(S, F, θ: Σ̄→Σ) \\ φ_{1} ∧ ⋯ ∧ φ_{k} \end{matrix}}{⋀_{s∈S} ∀x : θ(s) • Ψ_{s}(x)}

F = {f_{1} : s_{1}^{1} … s_{m_{1}}^{1} →s^{1}; …; f_{k}: s_{1}^{k} … s_{m_{k}}^{k} →s^{k}}, Ψ_{s_{j}} is a formula with one free variable x of sort θ(s_{j}), j = 1, …, k, φ_{j} = ∀x_{1} : θ(s_{1}^{j}), …, x_{m_{j}} : θ(s_{m_{j}}^{j})•

(D(θ(f_{j})(x_{1}, …, x_{m_{j}})) ∧ ⋀_{i=1,... ,m_{j}; s_{i}^{j}∈S} Ψ_{s_{i}^{j}}(x_{i}))

⇒ Ψ_{s_{j}} (θ(f_{j})(x_{1}, …, x_{m_{j}}))

(Sortgen-intro) \frac{φ_{1} ∧ ⋯ ∧ φ_{k} ⇒ ⋀_{s∈S} ∀x : θ(s) • p_{s}(x)}{(S, F, θ: Σ̄→Σ)}

F = {f_{1} : s_{1}^{1} … s_{m_{1}}^{1} →s^{1}; …; f_{k}: s_{1}^{k} … s_{m_{k}}^{k} →s^{k}}, for s ∈ S, the predicates p_{s} : θ(s) occur only in local assumptions, and for j = 1, …, k, φ_{j} = ∀x_{1} : θ(s_{1}^{j}), …, x_{m_{j}} : θ(s_{m_{j}}^{j})•

(D(θ(f_{j})(x_{1}, …, x_{m_{j}})) ∧ ⋀_{i=1,... ,m_{j}; s_{i}^{j}∈S} p_{s_{i}^{j}}(x_{i})) ⇒ p_{s_{j}} (θ(f_{j})(x_{1}, …, x_{m_{j}}))

Fig. 1. Deduction rules for Casl basic specifications

With sort generation constraints, inductive datatypes such as the natural numbers can be specified monomorphically (up to isomorphism). By Gödel’s incompleteness theorem, there cannot be a recursively axiomatized complete calculus for such systems.

Theorem 2. If sort generation constraints are used, the Casl logic is not complete. Moreover, there cannot be a recursively axiomatized sound and complete entailment system for many-sorted Casl basic specifications.

Instead of using the above calculus, it is also possible to use an encoding of the Casl logic into second order logic, see [34].

4 SUBSORTED BASIC SPECIFICATIONS

Casl allows the user to declare a sort as a subsort of another. In contrast to most other subsorted languages, Casl interprets subsorts as injective embeddings between carriers – not necessarily as inclusions. This allows for more general models in which values of a subsort are represented differently from values of the supersort, an example being integers (represented as 32-bit words) as a subsort of reals (represented using floating point). Furthermore, to avoid problems with modularity (as described in [21, 31]), there are no requirements like monotonicity, regularity or local filtration imposed on signatures. Instead, the use of overloaded functions and predicates in formulae of the Casl language is required to be sufficiently disambiguated, such that all parses have the same semantics.

4.1 Subsorted institution

In order to cope with subsorting, the institution for basic specifications presented in Section 3 has to be modified slightly. First, in Section 4.1.1, the category of signatures is defined (each signature is extended with a pre-order ≤ on its set of sorts) and a functor from this category into the category of many-sorted signatures is defined. Then, in Sections 4.1.2–4.1.4, the notions of models, sentences and satisfaction can be borrowed from the many-sorted institution via this functor. Technical details follow below, leading to the institution of subsorted partial first-order logic with sort generation constraints and equality (SubP CF OL^{=}).

4.1.1 Signatures

A subsorted signature Σ = (S, TF , PF , P, ≤) consists of a many-sorted signature (S, TF , PF , P) together with a reflexive transitive subsort relation ≤ on the set S of sorts.

For a subsorted signature, we define overloading relations for function and predicate symbols: Two function symbols f : w_{1} → s_{1} (or f : w_{1} →? s_{1}) and f : w_{2} → s_{2} (or f : w_{2} →? s_{2}) are in the overloading relation iff there exists a w ∈ S^{∗} and s ∈ S such that w ≤ w_{1}, w_{2} and s_{1}, s_{2} ≤ s. Similarly, two qualified predicate symbols p : w_{1} and p : w_{2} are in the overloading relation iff there exists a w ∈ S^{∗} such that w ≤ w_{1}, w_{2}.

Let Σ = (S, TF , PF , P, ≤) and Σ′ = (S′, TF′, PF′, P′, ≤′) be subsorted signatures. A subsorted signature morphism σ : Σ → Σ′ is a many-sorted signature morphism from (S, TF , PF , P) into (S′, TF′, PF′, P′) preserving the subsort relation and the overloading relations.

With each subsorted signature Σ = (S, TF , PF , P, ≤) we associate a manysorted signature Σ̂, which is the extension of the underlying many-sorted signature (S, TF , PF , P) with

• a total embedding function symbol em : s → s′ for each pair of sorts s ≤ s′ • a partial projection function symbol pr : s′ →? s for each pair of sorts s ≤ s′ • a unary membership predicate symbol in(s) : s′ for each pair of sorts s ≤ s′

It is assumed that the symbols used for injection, projection and membership are distinct and not used otherwise in Σ.

In a similar way, any subsorted signature morphism σ from Σ into Σ′ extends to a many-sorted signature morphism σ̂ from Σ̂ into Σ̂′.

The construction is a functor from the category of subsorted signatures SubSig into the category of many-sorted signatures Sign.

4.1.2 Models

For a subsorted signature Σ = (S, TF , PF , P, ≤), with embedding symbols em, projection symbols pr, and membership symbols in, the subsorted models for Σ are ordinary many-sorted models for Σ̂ satisfying a set Ax(Σ) of sentences ensuring that:

• Embedding functions are injective.

• The embedding of a sort into itself is the identity function.

• All compositions of embedding functions between the same two sorts are equal functions.

• Projection functions are injective when defined.

• Embedding followed by projection is identity.

• Membership in a subsort holds just when the projection to the subsort is defined.

• Embedding is compatible with those functions and predicates that are in the overloading relations.

Subsorted Σ-homomorphisms are ordinary many-sorted Σ̂-homomorphisms. Hence, the category of subsorted Σ-models SubMod(Σ) is a full subcategory of

Mod(Σ̂), i.e. SubMod(Σ) = Mod(Σ̂, Ax(Σ)).

The reduct of Σ′-models and Σ′-homomorphisms along a subsorted signature morphism σ from Σ into Σ′ is the many-sorted reduct along the signature morphism σ̂. Since subsorted signature morphisms preserve the overloading relations, this is well-defined and leads to a functor Mod(σ̂): SubMod(Σ′)→SubMod(Σ).

4.1.3 Sentences

For a subsorted signature Σ, the subsorted sentences are the ordinary many-sorted sentences for the associated many-sorted signature Σ̂.

Moreover, the subsorted translation of sentences along a subsorted signature morphism σ is the ordinary many-sorted translation along σ̂.

The syntax of the Casl language (cf. Sect. 5) allows the user to omit subsort injections, thus permitting the axioms to be written in a simpler and more intuitive way. Static analysis then determines the corresponding sentences of the underlying institution by inserting the appropriate injections.

4.1.4 Satisfaction

Since subsorted Σ-models and Σ-sentences are just certain many-sorted Σ̂-models and Σ̂-sentences, the notion of satisfaction for the subsorted case follows directly from the notion of satisfaction for the many-sorted case. Since reducts and sentence translation are ordinary many-sorted reducts and sentence translation, the satisfaction condition is satisfied for the subsorted case as well.

4.2 Borrowing of proofs

The proof calculus can borrowed from the many-sorted case. To prove that a Σsentence φ is a Σ-consequence of a set of assumptions Φ, one just has to prove that φ is a Σ̂-consequence of Φ and Ax(Σ), i.e.

Φ ⊢_{Σ} φ

if and only if

Φ ∪ Ax(Σ) ⊢_{Σ} φ

Soundness and (for the sublogic without sort generation constraints) completeness follows from the many-sorted case.

5 CASL LANGUAGE CONSTRUCTS

Since the level of syntactic constructs will be treated only informally in this paper, we just give a brief overview of the constructs for writing basic specifications (i.e. specifications in-the-small) in Casl. A detailed description can be found in the Casl Language Summary [26] and the Casl semantics [8].

The Casl language provides constructs for declaring sorts, subsorts, operations^{2} and predicates that contribute to the signature in the obvious way. Operations, predicates and subsorts can also be defined in terms of others; this leads to a corresponding declaration plus a defining axiom.

2 At the level of constructs, functions are called operations.

%list [ ], nil, ::

%prec { :: } < { ++ }

spec List [sort Elem] = free type List[Elem] ::= nil | :: (head :? Elem; tail :? List[Elem]); sort NEList[Elem] = {L : List[Elem] • ¬L = nil}; op ++ : List[Elem] × List[Elem] → List[Elem]; forall e : Elem; K , L : List[Elem]

• nil ++L = L %(concat nil)% • (e :: K ) ++L = e :: K ++L %(concat cons)%

end

Fig. 2. Specification of lists over an arbitrary element sort in Casl.

Operation and predicate symbols may be overloaded; this can lead to ambiguities in formulas. A formula is well-formed only if there is a unique way of consistently adding profile qualifications, up to equivalence with respect to the overloading relations.

For operations and predicates, mixfix syntax is provided. Precedence and associativity annotations may help to disambiguate terms containing mixfix symbols. There is also a syntax for literals such as numbers and strings, which allows the usual datatypes to be specified purely in Casl, without the need for magic built-in modules.

Binary operations can be declared to be associative, commutative, idempotent, or to have a unit. This leads to a corresponding axiom, and, in the case of associativity, to an associativity annotation.

The type, free type and generated type constructs allow the concise description of datatypes. These are expanded into the declaration of the corresponding constructor and selector operations and axioms relating the selectors and constructors. In the case of generated and free datatypes, a sort generation constraint is also produced. Free datatypes additionally lead to axioms that assert the injectivity of the constructors and the disjointness of their images.

A typical Casl specification is shown in Fig. 2. The translation of Casl constructs to the underlying mathematical concepts is formally defined in the Casl semantics [8], which gives the semantics of language constructs in two parts. The static semantics checks well-formedness of a specification and produces a signature as result, failing to produce any result for ill-formed phrases. The model semantics provides the corresponding model-theoretic part of the semantics and produces a class of models as a result, and is intended to be applied only to phrases that are well-formed according to the static semantics. A statically well-formed phrase may still be ill-formed according to the model semantics, and then no result is produced.

6 STRUCTURED SPECIFICATIONS

The Casl structuring concepts and constructs and their semantics do not depend on a specific framework of basic specifications. This means that the design of manysorted and subsorted Casl specifications as explained in the previous sections is orthogonal to the design of structured specifications that we are now going to describe (this also holds for the remaining parts of Casl: architectural specifications and libraries). In this way, we achieve that the Casl basic specifications as given above can be restricted to sublanguages or extended in various ways (or even replaced completely) without the need to reconsider or to change syntax and semantics of structured specifications. The central idea for achieving this form of genericity is the notion of institution introduced in Section 2. Indeed, many different logics, including first-order [19], higher-order [12], polymorphic [?], modal [15, 53], temporal [18], process [18], behavioural [10], and object-oriented [51, 20, 27, 52, 2] logics have been shown to be institutions.

   SPEC ::= BASIC-SPEC
           | SPEC_{1} and SPEC_{2}

| SPEC with σ
| SPEC hide σ
| SPEC_{1} then free { SPEC_{2} }

Fig. 3. Simplified syntax of Casl structured specifications

6.1 Syntax and semantics of structured specifications

Given an arbitrary but fixed institution with unions, it is now possible to define structured specifications. Their syntax is given in Fig. 3. The syntax of basic specifications BASIC-SPEC (as well as that of signature morphisms σ) is left unexplained, since it is provided together with the institution.

Fig. 4 shows the semantics of structured specifications [47, 8]. The static semantics is shown on the left of the figure, using judgements of the form ⊢ phrase ⊳result (read: phrase statically elaborates to result). The model semantics is shown on the right, using judgements of the form ⊢ phrase ⇒ result (read: phrase evaluates to result).

As expected, we assume that every basic specification (statically) determines a signatures and a (finite) set of axioms, which in turn determine the class of models of this specification.

Using the model semantics, we can define semantical entailment as follows: a well-formed Σ-specification SP entails a Σ-sentence φ, written SP ⊧_{Σ} φ, if φ is satisfied in all SP-models. Moreover, we also have a simple notion of refinement between specifications: SP_{1} refines to SP_{2}, written SP_{1} ⇝ ⇝ SP_{2}, if every SP_{2}-model is also an SP_{1}-model. Given a Σ_{1}-specification SP_{1} and a Σ_{2}-specification SP_{2}, a

     \frac{⊢ BASIC-SPEC ⊳ ⟨Σ, Γ⟩}{⊢ BASIC-SPEC ⊳ Σ}  \frac{⊢ BASIC-SPEC ⊳ ⟨Σ, Γ⟩ M = \{M ∈ Mod(Σ) | M ⊧ Γ\}}{⊢ BASIC-SPEC ⇒ M}

\frac{⊢ SP_{1} ⊳ Σ_{1} ⊢ SP_{2} ⊳ Σ_{2} Σ_{1} ∪ Σ_{2} is defined}{⊢ SP_{1} and SP_{2} ⊳ Σ_{1} ∪ Σ_{2}}  \frac{⊢ SP_{1} ⊳ Σ_{1} ⊢ SP_{2} ⊳ Σ_{2} Σ′ = Σ_{1} ∪ Σ_{2} is defined ⊢ SP_{1} ⇒ M_{1} ⊢ SP_{2} ⇒ M_{2} M=\{M ∈ Mod(Σ′) |M|_{Σ_{i}} ∈ M_{i}, i = 1, 2\}}{⊢ SP_{1} and SP_{2} ⇒ M}

\frac{⊢ SP ⊳ Σ}{⊢ SP with σ: Σ→Σ′ ⊳ Σ′}  \frac{⊢ SP ⊳ Σ ⊢ SP ⇒ M M′ = \{M ∈ Mod(Σ′) | M|_{σ} ∈ M\}}{⊢ SP with σ: Σ→Σ′ ⇒ M′}

\frac{⊢ SP ⊳ Σ′}{⊢ SP hide σ: Σ→Σ′ ⊳ Σ}  \frac{\begin{matrix}⊢ SP ⊳ Σ′ ⊢ SP ⇒ M \\ M′ = \{M|_{σ} | M ∈ M\} \end{matrix}}{⊢ SP hide σ: Σ→Σ′ ⇒ M′}

\frac{⊢ SP_{1} ⊳ Σ_{1} ⊢ SP_{2} ⊳ Σ_{2} Σ_{1} ⊆ Σ_{2}}{⊢ SP_{1} then free \{ SP_{2} \} ⊳ Σ_{2}}

\frac{⊢ SP_{1} ⊳ Σ_{1} ⊢ SP_{2} ⊳ Σ_{2} ι: Σ_{1} →Σ_{2} is the inclusion ⊢ SP_{1} ⇒ M_{1} ⊢ SP_{2} ⇒ M_{2} M′ = \{M | M is Mod(ι)-free over M _{ι} in M_{2}\}}{⊢ SP_{1} then free \{ SP_{2} \} ⇒ M′}

M being Mod(ι)-free over M _{ι} in M_{2} means that for each model M′ ∈ M_{2} and model morphism h: M _{ι} → M′ _{ι}, there exists a unique model morphism h^{#} : M →M′ with h^{#} _{ι} = h.

Fig. 4. Semantics of structured specifications

specification morphism σ: SP_{1} → SP_{2} is a signature morphism σ: Σ_{1} → Σ_{2} such that for each SP_{2}-model M, M|_{σ} is an SP_{1}-model. Note that σ: SP_{1} → SP_{2} is a specification morphism iff SP_{1} ⇝ ⇝ SP_{2} hide σ.

The above language is a somewhat simplified version of Casl structured specifications. The first simplification concerns the way signature morphisms are given. It is quite inconvenient to be forced to always write down a complete signature morphism, listing explicitly how each fully qualified symbol is mapped. As a solution to this problem, Casl provides a notion of symbol maps, based on an appropriate notion of institution with symbols. Symbol maps are a very concise notation for signature morphisms. Qualifications with profiles, symbols that are mapped identically and even those whose mapping is determined uniquely may be omitted. Details can be found in [8, 33].

The second simplification concerns the fact that it is often very convenient to define specifications as extensions of existing specifications. For example, in SPEC then free { SPEC′ }, typically SPEC′ is an extension of SPEC, and one does not really want to repeat all the declarations in SPEC again in SPEC′ just for the sake of turning SPEC′ into a self-contained specification. Therefore, Casl has a construct SP then SP′, where SP′ can be a specification fragment that is interpreted in the context (referred to as the local environment) coming from SP. Again, details can be found in [8].

6.2 A proof calculus for structured specifications

As explained above, the semantics of Casl structured specifications is parameterized over an institution providing the semantics of basic specifications. The situation with the proof calculus is similar: here, we need a logic, i.e. an institution equipped with an entailment system. Based on this, it is possible to design a logic independent proof calculus [13] for proving entailments of the form SP ⊢ φ, where SP is a structured specification and φ is a formula, see Fig. 5. Fig. 6 shows an extension of the structured proof calculus to refinements between specifications. Note that for the latter calculus, an oracle for conservative extensions is needed. A specification morphism σ: SP_{1} →SP_{2} is conservative iff each SP_{1}-model is the σ-reduct of some SP_{2}-model.^{3}

(CR) \frac{\{SP ⊢ φ_{i}\}_{i∈I} \{φ_{i}\}_{i∈I} ⊢ φ}{SP ⊢ φ} (basic) \frac{φ ∈ Γ}{⟨Σ, Γ⟩ ⊢ φ}
(sum1 ) \frac{SP_{1} ⊢ φ}{SP_{1} and SP_{2} ⊢ ι_{1}(φ)}  (sum2 ) \frac{SP_{2} ⊢ φ}{SP_{1} and SP_{2} ⊢ ι_{2}(φ)}

(trans) \frac{SP ⊢ φ}{SP with σ ⊢ σ(φ)}  (derive) \frac{SP ⊢ σ(φ)}{SP hide σ ⊢ φ}

Fig. 5. Proof calculus for entailment in structured specifications

Theorem 3 (Soundness [13]). The calculus for structured entailment is sound, i.e. SP ⊢ φ implies SP ⊧ φ. Also, the calculus for refinement between finite structured specifications is sound, i.e. SP_{1} ⇝ SP_{2} implies SP_{1} ⇝ ⇝ SP_{2}.

3 Besides this model-theoretic notion of conservativeness, there also is a weaker consequence-theoretic notion: SP_{2} ⊧ σ(φ) implies SP_{1} ⊧ φ, and a proof-theoretic notion coinciding with the consequence-theoretic one for complete logics: SP_{2} ⊢ σ(φ) implies SP_{1} ⊢ φ. For the calculus of refinement, we need the model-theoretic notion.

(Basic) \frac{SP ⊢ Γ}{⟨Σ, Γ⟩ ⇝ SP} (Sum) \frac{SP_{1} with ι_{1} ⇝ SP SP_{2} with ι_{2} ⇝ SP}{SP_{1} and SP_{2} ⇝ SP}

(Trans_{1}) \frac{SP ⇝ SP′ with θ θ = σ^{−1}}{SP with σ ⇝ SP′} (Trans_{2}) \frac{SP ⇝ SP′ hide σ}{SP with σ ⇝ SP′}

(Derive) \frac{SP ⇝ SP′′}{SP hide σ ⇝ SP′} if σ: SP′ →SP′′ is a conservative extension

(Trans-equiv) \frac{(SP with σ) with θ ⇝ SP′}{SP with σ;θ ⇝ SP′}

Fig. 6. Proof calculus for refinement of structured specifications

Before we can state a completeness theorem, we need to formulate some technical assumptions on the underlying institution I.

An institution has the Craig interpolation property, if for any pushout

[figure: Σ; σ_{1}; Σ_{1}; Σ_{2}; σ_{2}; θ_{1}; Σ′; θ_{2}]

any Σ_{1}-sentence φ_{1} and any Σ_{2}-sentence φ_{2} with

θ_{2}(φ_{1}) ⊧ θ_{1}(φ_{2}),

there exists a Σ-sentence φ (called the interpolant) such that

φ_{1} ⊧ σ_{1}(φ) and σ_{2}(φ) ⊧ φ_{2}.

A cocone for a diagram in Sign is called (weakly) amalgamable if it is mapped to a (weak) limit under Mod. I (or Mod) admits (finite) (weak) amalgamation if (finite) colimit cocones are (weakly) amalgamable, i.e. if Mod maps (finite) colimits to (weak) limits. An important special case is pushouts in the signature category, which are prominently used for instance in instantiations of parameterized specifications. (Recall also that finite limits can be constructed from pullbacks and terminal objects, so that finite amalgamation reduces to preservation of pullbacks and terminal objects — dually: pushouts and initial objects). Here, the (weak) amalgamation property requires that a pushout

[figure: Σ; Σ_{1}; Σ_{2}; Σ_{R}]

in Sign is mapped by Mod to a (weak) pullback

Mod(Σ) \underline{}Mod(Σ_{1})

[figure: Mod(Σ_{2}); Mod(Σ_{R})]

of categories. Explicitly, this means that any pair (M_{1}, M_{2}) ∈ Mod(Σ_{1})×Mod(Σ_{2}) that is compatible in the sense that M_{1} and M_{2} reduce to the same Σ-model can be amalgamated to a unique (or weakly amalgamated to a not necessarily unique) Σ_{R}-model M (i.e., there exists a (unique) M ∈ Mod(Σ_{R}) that reduces to M_{1} and M_{2}, respectively), and similarly for model morphisms.

An institution has conjunction, if for any Σ-sentences φ_{1} and φ_{2}, there is a Σsentence φ that holds in a model iff φ_{1} and φ_{2} hold. The notion of an institution having implication is defined similarly.

Theorem 4 (Completeness [13]). Under the assumptions that

• the institution has the Craig interpolation property,

• the institution admits weak amalgamation,

• the institution has conjunction and implication and

• the logic is complete,

the calculi for structured entailment and refinement between finite structured specifications are complete.

Actually, the assumption of Craig interpolation and weak amalgamation can be restricted to those diagrams for which it is really needed. Details can be found in [13].

Notice though that even a stronger version of the interpolation property, namely Craig-Robinson interpolation as in [17], still needs closure of the set of sentences under implication in order to ensure the completeness of the above compositional proof system.

A problem with the above result is that Craig interpolation often fails, e.g. it does not hold for the Casl institution SubP CF OL^{=} (only for the sublanguage without subsorts and sort-injective signature morphisms, see [11]). This problem may be overcome by adding a “global” rule to the calculus, which does a kind of normal form computation, while maintaining the structure of specifications to guide proof search as much as possible; see [35].

Checking conservativity in the CASL institution The proof rules for refinement are based on an oracle checking conservativeness of extensions. Hence, logic-specific rules for checking conservativeness are needed. For Casl, conservativeness can be checked by syntactic criteria: e.g. free types and recursive definitions over them are always conservative. But more sophisticated rules are also available, see [37]. Note that checking conservativeness is at least as complicated as checking non-provability: for a Σ-specification SP, SP |̸= φ iff SP and ⟨Σ, {¬φ}⟩ is consistent iff SP and ⟨Σ, {¬φ}⟩ is conservative over the empty specification. Hence, even checking conservativeness in first-order logic is not recursively enumerable, and thus there is no recursively axiomatized complete calculus for this task.^{4}

Proof rules for free specifications An institution independent proof theory for free specifications has not been developed yet (if this should be feasible at all). Hence, for free specifications, one needs to develop proof support for each institution separately. For the Casl institution, this has been done in [37]. The main idea is just to mimick a quotient term algebra construction, and to restrict proof support to those cases (e.g. Horn clause theories) where the free model is given by such a construction. Details can be found in [37].

6.3 Named and parameterized specifications and views

Structured specifications may be named, so that the reuse of a specification may be replaced by a reference to it through its name. A named specification may declare some parameters, the union of which is extended by a body; it is then called generic. A reference to a generic specification should instantiate it by providing, for each parameter, an argument specification together with a fitting morphism from the parameter to the argument specification. Fitting may also be achieved by (explicit) use of named views between the parameter and argument specifications. The union of the arguments, together with the translation of the generic specification by an expansion of the fitting morphism, corresponds to a pushout construction—taking into account any explicit imports of the generic specification, which allow symbols used in the body to be declared also by arguments.

Since parameterization may be expressed in terms of union and translation, we omit its semantics and proof rules here.

Semantically, a view v: SP_{1} →SP_{2} from a Σ_{1}-specification SP_{1} to a Σ_{2}-specifica-tion SP_{2} is basically is a specification morphism σ: SP_{1} → SP_{2}, leading to a proof obligation SP_{1} ⇝ SP_{2} hide σ. A similar proof obligation is generated for anonymous instantiations of parameterized specifications (i.e. not given by a named view).

Naming specifications and referencing them by name leads to graphs of specifications. This is formalized as a so-called development graph [35, 37], which express sharing between specifications, thereby leading to a more efficient proof calculus, and providing management of proof obligations and proofs for structured specification, as well as management of change.

4 The situation is even more subtle. The model-theoretic notion of conservative extension (or, equivalently, of refinement between specifications involving hiding) corresponds to second-order existential quantification. It is well-known that the semantics of second-order logic depends on the background set theory [28]. For example, one can build a specification and its extension that is conservative (or equivalently, provide another specification to which it refines) iff the continuum hypothesis holds — a question that is undecidable on the basis of our background metatheory ZF CU.

7 ARCHITECTURAL SPECIFICATIONS

Architectural specifications in Casl provide a means of stating how implementation units are used as building blocks for larger components. (Dynamic interaction between modules and dynamic changes of software structure are currently beyond the scope of this approach.)

Units are represented as names to which a specification is associated. Such a named unit is to be thought of as an arbitrarily selected model of the specification. Units may be parameterized, where specifications are associated with both the parameters and the result. The result specification is required to extend the parameter specifications. A parameterized unit is to be understood as a function which, given models of the parameter specifications, outputs a model of the result specification; this function is required to be persistent in the sense that reducing the result to the parameter signatures reproduces the parameters.

Units can be assembled via unit expressions which may contain operations such as renaming or hiding of symbols, amalgamation of units, and application of a parameterized unit. Terms containing such operations will only be defined if symbols that are identified, e.g. by renaming them to the same symbol or by amalgamating units that have symbols in common, are also interpreted in the same way in all “collective” models of the units defined so far.

An architectural specification consists of declarations and/or definitions of a number of units, together with a way of assembling them to yield a result unit.

Example 5. A (fictitious) specification structure for a compiler might look roughly as follows:

Identifier  List
[figure]

ProgramText

[figure]
AbstractSyntax  SymbolTable
[figure]
Parser  StaticAnalyser  CodeGenerator
[figure]
Compiler

(The arrows indicate the extension relation between specifications.) An architectural specification of the compiler in Casl might have the following form:

arch spec BuildCompiler = units

I : Identifier with sorts Identifier, Keyword;
L : Elem → List[Elem];
IL = L[I fit sort Elem ↦ Identifier]
KL = L[I fit sort Elem ↦ Keyword]
PT : ProgramText given IL, KL;
AS : AbstractSyntax given PT ;
ST : SymbolTable given PT ;
P : Parser given AS;
SA : StaticAnalyser given AS, ST ;
CG : CodeGenerator given ST

result P and SA and CG end

(Here, the keyword with is used to just list some of the defined symbols. The keyword given indicates imports.) According to the above specification, the parser, the static analyser, and the code generator would be constructed building upon a given abstract syntax and a given mechanism for symbol tables, and the compiler would be obtained by just putting together the former three units. Roughly speaking, this is only possible (in a manner that can be statically checked) if all symbols that are shared between the parser, the static analyser and the code generator already appear in the units for the abstract syntax or the symbol tables — otherwise, incompatibilities might occur that make it impossible to put the separately developed components together. For instance, if both StaticAnalyser and CodeGenerator declare an operation lookup that serves to retrieve symbols from the symbol table, then the corresponding implementations might turn out to be substantially different, so that the two components fail to be compatible. Of course, this points to an obvious flaw in the architecture: lookup should have been declared in SymbolTable.

Consider an institution with unions I = (Sign, Sen, Mod, ⊧). We assume that the signature category is finitely cocomplete and that the institution admits amalgamation. We also assume that signature unions are exhaustive in the sense that given two signatures Σ_{1} and Σ_{2} and their union Σ_{1} ⟶^{ι_{1}} (Σ_{1} ∪ Σ_{2}) ⟵^{ι_{2}} Σ_{2}, for any models M_{1} ∈ Mod(Σ_{1}) and M_{2} ∈ Mod(Σ_{2}), there is at most one model M ∈ Mod(Σ_{1}∪Σ_{2}) such that M _{ι_{1}} = M_{1} and M _{ι_{2}} = M_{2}. In such a framework we formally present a small but representative subset of Casl architectural specifications. The fragment — or rather, its syntax — is given in Fig. 7.

Architectural specifications: ASP ::= arch spec Dcl^{∗} result T Unit declarations: Dcl ::= U : SP | U : SP_{1} ⟶^{τ} SP_{2} Unit terms: T ::= U | U [T fit σ] | T_{1} and T_{2}

Fig. 7. A fragment of the architectural specification formalism

Example 5 additionally uses unit definitions and imports. Unit definitions U = T introduce a (non-parameterized) unit and give its value by a unit term. Imports can be regarded as syntactical sugar for a parameterized unit which is instantiated only once: if U_{1} : SPEC_{1}, then

U_{2} : SPEC_{2} given U_{1}

abbreviates

           U′_{2} : SPEC_{1} → SPEC_{2} ;

U_{2} =U′_{2} [U_{1} ].

We now sketch the formal semantics of our language fragment and show how correctness of such specifications may be established.

7.1 Semantics of architectural specifications

The semantics of architectural specifications introduced above is split into their static and model semantics, in very much the same way as for structured specifications in Sect. 6.

Unit terms are statically elaborated in a static context C_{st} = (P_{st}, B_{st}), where P_{st} maps parameterized unit names to signature morphisms and B_{st} maps nonparameterized unit names to their signatures. We require the domains of P_{st} and B_{st} to be disjoint. The empty static context that consists of two empty maps will be written as C_{st}^{∅}. Given an initial static context, the static semantics for unit declarations produces a static context by adding the signature for the newly introduced unit, and the static semantics for unit terms determines the signature for the resulting unit.

In terms of the model semantics, a (non-parameterized) unit M over a signature Σ is just a model M ∈ Mod(Σ). A parameterized unit F over a parameterized unit signature τ : Σ_{1} → Σ_{2} is a persistent partial function F : Mod(Σ_{1}) ⇀ Mod(Σ_{2}) (i.e. F (M) _{τ} = M for each M ∈ Dom(F)).

The model semantics for architectural specifications involves interpretations of unit names. These are given by unit environments E, i.e. finite maps from unit names to units as introduced above. On the model semantics side, the analogue of a static context is a unit context C, which is just a class of unit environments, and can be thought of as a constraint on the interpretation of unit names. The unconstrained unit context, which consists of all environments, will be written as C^{∅}. The model semantics for unit declarations modifies unit contexts by constraining the environments to interpret the newly introduced unit names as determined by their specification or definition.

A unit term is interpreted by a unit evaluator UEv, a function that yields a unit when given a unit environment in the unit context (the unit environment serves to interpret the unit names occurring in the unit term). Hence, the model semantics for a unit term yields a unit evaluator, given a unit context.

The complete semantics is given in Figures 8 (static semantics) and 9 (model semantics) where we use some auxiliary notation: given a unit context C, a unit

\frac{⊢ UDD^{∗} ⊳ C_{st} C_{st} ⊢ T ⊳ Σ}{⊢ arch spec UDD^{∗} result T ⊳ (C_{st}, Σ)}

\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{⊢ SP ⊳ Σ U ∉ (Dom(P_{st}) ∪ Dom(B_{st}))}{(P_{st}, B_{st}) ⊢ U : SP ⊳ (P_{st}, B_{st} + \{U ↦ Σ\})}

\frac{⊢ SP_{1} ⊳ Σ_{1} ⊢ SP_{2} ⊳ Σ_{2} τ : Σ_{1} → Σ_{2} U ∉ (Dom(P_{st}) ∪ Dom(B_{st}))}{(P_{st}, B_{st}) ⊢ U : SP_{1} ⟶^{τ} SP_{2} ⊳ (P_{st} + \{U ↦ τ\}, B_{st})}

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

\frac{P_{st}(U ) = τ : Σ → Σ′ C_{st} ⊢ T ⊳ Σ_{T} σ: Σ→Σ_{T} (τ′ : Σ_{T} → Σ′_{T} , σ′ : Σ′ → Σ′_{T}) is the pushout of (σ, τ)}{(P_{st}, B_{st}) ⊢ U [T fit σ] ⊳ Σ′_{T}}

\frac{C_{st} ⊢ T_{1} ⊳ Σ_{1} C_{st} ⊢ T_{2} ⊳ Σ_{2} Σ = Σ_{1} ∪ Σ_{2} with inclusions ι_{1} : Σ_{1} → Σ, ι_{2} : Σ_{2} → Σ}{(P_{st}, B_{st}) ⊢ T_{1} and T_{2} ⊳ Σ}

Fig. 8. Static semantics of architectural specifications

name U and a class V,

C × {U ↦ V} := {E + {U ↦ V } | E ∈ C, V ∈ V},

where E + {U ↦ V } maps U to V and otherwise behaves like E. The model semantics assumes that the static semantics has been successful on the constructs considered; we use the notations introduced by this derivation of the static semantics in the model semantics rules whenever convenient.

The model semantics is easily seen to be compatible with the static semantics in the following sense: we say that C fits C_{st} = (P_{st}, B_{st}), if, whenever B_{st}(U ) = Σ and E ∈ C, then E(U ) is a Σ-model, and a corresponding condition holds for P_{st}. Obviously, C^{∅} fits C_{st}^{∅}. Now if C fits C_{st}, then C_{st} ⊢ T ⊳ Σ and C ⊢ T ⇒ UEv imply that UEv(E) is a Σ-model for each E ∈ C. Corresponding statements hold for the other syntactic categories (unit declarations, architectural specifications).

We say that an architectural specification is internally correct (or simply: correct) if it has both static and model semantics. Informally, this means that the architectural design the specification captures is correct in the sense that any realization of the units according to their specifications allows us to construct an overall result by performing the construction prescribed by the result unit term.

Checking correctness of an architectural specification requires checking that all the rules necessary for derivation of its semantics may indeed be applied, that is, all their premises can be derived and the conditions they capture hold. Perhaps the only steps which require further discussion are the rules of the model semantics for unit application and amalgamation in Fig. 9. Only there do some difficult premises occur, marked by (∗), (∗∗) and (∗∗∗), respectively. All the other premises of the semantic rules are “easy” in the sense that they largely just pass on the information collected about various parts of the given phrase, or perform a very simple check that names are introduced before being used, signatures fit as expected, etc.

First we consider the premises (∗∗) and (∗∗∗) in the rules for unit application and amalgamation, respectively. They impose “amalgamability requirements”, necessary to actually build the expected models by combining the simpler models, as indicated. Such requirements are typically expected to be at least partially discharged by static analysis — similarly to the sharing requirements present in some programming languages (cf. e.g. Standard ML [42]). Under our assumptions, the premise (∗∗) may simply be skipped, as it always holds (since all parameterized units are persistent functions, E(U )(UEv(E) _{σ}) _{τ} = UEv(E) _{σ}, and so the required unique model M ∈ Mod(Σ′_{T}) exists by the amalgamation property of the institution). The premise (∗∗∗) may fail though, and a more subtle static analysis of the dependencies between units may be needed to check that it holds for a given construct.

The premise (∗) in the rule for application of a parameterized unit requires that the fitting morphism correctly “fits” the actual parameter as an argument for the parameterized unit. To verify this, one typically has to prove that the fitting morphism is a specification morphism from the argument specification to the specification of the actual parameter. Similarly as with the proof obligations arising for instantiations of parameterized specifications discussed in Sect. 6.3, this in general requires some semantic or proof-theoretic reasoning. Moreover, a suitable calculus is needed to determine a specification for the actual parameter. One naive attempt to provide it might be to build such a specification inductively for each unit term using directly specifications of its components. Let SP_{T} be such a specification for the term T. In other words, verification conditions aside:

• SP_{U} is SP, where U : SP is the declaration of U ; • SP_{T_{1} and T_{2}} is (SP_{T_{1}} and SP_{T_{2}});

• SP_{U [T fit σ]} is ((SP_{T} with τ′) and (SP′ with σ′)), where U : SP ⟶^{τ} SP′ is the declaration of U and (τ′, σ′) is the pushout of (σ, τ), as in the corresponding rule of the static semantics.

It can easily be seen that SP_{T} so determined is indeed a correct specification for T , in the sense that if C_{st} ⊢ T ⊳ Σ and C ⊢ T ⇒ UEv then ⊢ SP_{T} ⊳ Σ and ⊢ SP_{T} ⇒ M with UEv(E) ∈ M for each E ∈ C. Therefore, we could replace the requirement (∗) by SP ⇝ ⇝ SP_{T} hide σ.

However, this would be highly incomplete. Consider a trivial example:

units

U : {sort s; op a : s}
ID : {sort s; op b : s} → {sort s; op b : s}
F : {sort s; op a, b : s; axiom a = b} → …

result F [ U and ID[U fit b ↦ a] ]

The specification we obtain for the argument unit term of F does not capture that fact that a = b holds in all units that may actually arise as the argument for F here. The problem is that the specification for a unit term built as above entirely disregards any dependencies and sharing that may occur between units denoted by unit terms, and so is often insufficient to verify correctness of unit applications. Hence, this first try to calculate specifications for architectural unit terms turns out to be inadequate, and a more complex form of architectural verification is needed.

7.2 Verification

The basic idea behind verification for architectural specifications is that we want to extend the static information about units to capture their properties by an additional specification. However, as discussed at the end of the previous section, we must also take into account sharing between various unit components, resulting from inheritance of some unit parts via for instance parameterized unit applications. To capture this, we accumulate information on non-parameterized units in a single global signature Σ_{G}, and represent non-parameterized unit signatures as morphisms into this global signature, assigning them to unit names by a map B_{v}. The additional information resulting from the unit specifications will be accumulated in a single global specification SP_{G} over this signature (i.e., we will always have ⊢ SP_{G} ⊳ Σ_{G}). Finally, we will of course store the entire specification for each parameterized unit, assigning them to parameterized unit names by a map P_{v}. This results in the concept of a verification context C_{v} = (P_{v}, B_{v}, SP_{G}). A static unit context ctx(C_{v}) = (P_{st}, B_{st}) may easily be extracted from such an extended one: for each U ∈ Dom(B_{v}), B_{st}(U ) = Σ, where B_{v}(U ) = i : Σ → Σ_{G}, and for each U ∈ Dom(P_{v}), P_{st}(U ) = τ, where P_{v}(U ) = SP_{1} ⟶^{τ} SP_{2}.

Given a morphism θ: Σ_{G} → Σ′_{G} that extends the global signature (or a global specification morphism θ: SP_{G} → SP′_{G}) we write B_{v};θ for the corresponding extension of B_{v} (mapping each U ∈ Dom(B_{v}) to B_{v}(U );θ). C_{v}^{∅} is the “empty” verification context (with the initial global specification^{5}).

The intuition introduced above is reflected in the forms of verification judgments, and captured formally by the verification rules:

⊢ ASP :: SP

Architectural specifications yield a specification of the result.

C_{v} ⊢ Dcl :: C′_{v}

In a verification context, unit declarations yield a new verification context.

(P_{v}, B_{v}, SP_{G}) ⊢ T :: Σ ⟶^{i} SP′_{G} ⟵^{θ} SP_{G}

In a verification context, unit terms yield their signature embedded into a new global specification, obtained as an indicated extension of the old global specification.

The verification rules to derive these judgments are in Fig. 10, with diagrams helping to read the more complicated rules for unit application and amalgamation in Fig. 11.

It should be easy to see that the verification semantics subsumes (in the obvious sense) the static semantics: a successful derivation of the verification semantics ensures a successful derivation of the static semantics with results that may be extracted from the results of the verification semantics in the obvious way.

More crucially, a successful derivation of the verification semantics on an architectural specification ensures a successful derivation of the model semantics, and hence the correctness of the architectural specification.

To state this more precisely, we need an extension to verification contexts of the notion that a unit context fits a static context: a unit context C_{v} fits a verification context C_{v} = (P_{v}, B_{v}, SP_{G}), where ⊢ SP_{G} ⇒ M_{G}, if

• for each E ∈ C and U ∈ Dom(P_{v}) with P_{v}(U ) = SP ⟶^{τ} SP′, where ⊢ SP ⇒ M and ⊢ SP′ ⇒ M′, we have E(U )(M) ∈ M′ for all M ∈ M, and

• for each E ∈ C, there exists M_{G} ∈ M_{G} such that for all U ∈ Dom(B_{v}), E(U ) = M_{G} _{B_{v} (U )}; we say then that E is witnessed by M_{G}.

Now, the following claims follow by induction:

• For every architectural specification ASP, if ⊢ ASP :: SP with ⊢ SP ⇒ M then ⊢ ASP ⇒ (C, UEv) for some unit context C and unit evaluator UEv such that UEv(E) ∈ M for all E ∈ C.

• For any unit declaration Dcl and verification context C_{v}, if C_{v} ⊢ Dcl :: C′_{v} then for any unit context C that fits C_{v}, C ⊢ Dcl ⇒ C′ for some unit context C′ that fits C′_{v}; this generalizes to sequences of unit declarations in the obvious way.

5 More precisely, this is the basic specification consisting of the initial signature with no axioms.

• For any unit term T and verification context C_{v} = (P_{v}, B_{v}, SP_{G}), where ⊢ SP_{G} ⇒ M_{G}, if C_{v} ⊢ T :: Σ ⟶^{i} SP′_{G} ⟵^{θ} SP_{G}, where ⊢ SP′_{G} ⇒ M′_{G}, then for any unit context C that fits C_{v}, C ⊢ T ⇒ UEv for some unit evaluator UEv such that for each E ∈ C witnessed by M_{G} ∈ M_{G}, there exists a model M′_{G} ∈ M′_{G} such that M′_{G} _{θ} = M_{G} and M′_{G} _{i} = UEv(E).

In particular this means that a successful derivation of the verification semantics ensures that in the corresponding derivation of the model semantics, whenever the rules for unit application and amalgamation are invoked, the premises marked by (∗), (∗∗) and (∗∗∗) hold. This may also be seen somewhat more directly:

(∗) Given the above relationship between verification and model semantics, the requirement (∗) in the model semantics rule for unit application follows from the requirement that SP with σ;i ⇝ SP′_{G} in the corresponding verification rule.

(∗∗) As pointed out already, the premises marked by (∗∗) may be removed by the assumption that the institution we work with admits amalgamation.

(∗∗∗) Given the above relationship between verification and model semantics, the existence of models required by (∗∗∗) in the model semantics rule for unit amalgamation can be shown by gradually constructing a compatible family of models over the signatures in the corresponding diagram in Fig. 11 (this requires amalgamation again); the uniqueness of the model so constructed follows from our assumption on signature union.

Note that only checking the requirement (∗) relies on the information gathered in the specifications built for unit terms by the verification semantics. The other requirements are entirely “static” in the sense that they may be checked also if we replace specifications by their signatures. This may be used to further split the verification semantics into two parts: an extended static analysis, performed without taking specifications into account, but considering in detail all the mutual dependencies between units involved to check properties like those labeled by (∗∗) and (∗∗∗); and a proper verification semantics aimed at considering unit specifications and deriving specifications for unit terms from them. See [54] for details.

7.3 Enriched Casl, diagram semantics and the cell calculus

The verification semantics of architectural specifications presented in the previous section crucially depends on amalgamation in the underlying institution. However, the Casl institution fails to have this property:

Example 6. The simplest case where amalgamation fails is the following: let Σ be the signature with sorts s and t and no operations, and let Σ_{1} be the extension of Σ by the subsort relation s ≤ t. Then the pushout

[figure: Σ; Σ_{1}; Σ_{1}; Σ_{1}]

in SubSig fails to be amalgamable (since two models of Σ_{1}, compatible w.r.t. the inclusion of Σ, may interpret the subsort injection differently).

The solution is to embed the Casl institution into an institution that enjoys the amalgamation property. The main idea in the definition of the required extended institution is to generalize pre-orders of sorts to categories of sorts, i.e. to admit several different subsort embeddings between two given sorts; this gives rise to the notion of enriched Casl signature. Details can be found in [50]. This means that before a Casl architectural specification can be statically checked and verification conditions can be proved, it has to be translated to enriched Casl, using the embedding.

One might wonder why the mapping from subsorted to many-sorted specifications introduced in Sect. 4 is not used instead of introducing enriched Casl. Indeed, this is possible. However, enriched Casl has the advantage of keeping the subsorting information entirely static, avoiding any axioms to capture the built-in structural properties, as would be the case with the mapping from Sect. 4.

This advantage plays a role in the so-called diagram semantics of architectural specifications. It replaces the global signatures that are used in the static semantics by diagrams of signatures and signature morphisms, see [8]. In the “extended static part” of the verification semantics, the commutativity conditions concerning signature morphisms into the global signature have then to be replaced by modeltheoretic amalgamation conditions. Given an embedding into an institution with amalgamation such as the one discussed above, the latter conditions are equivalent to factorization conditions of the colimit of the embedded diagram. For (enriched) Casl, these factorization conditions can be dealt using a calculus (the so-called cell calculus) for proving equality of morphisms and symbols in the colimit; see [25]. A verification semantics without reference to overall global specifications (which relies on the amalgamation property) and consequently with more “local” verification conditions is yet to be worked out.

8 REFINEMENT

The standard development paradigm of algebraic specification [5] postulates that formal software development begins with a formal requirement specification (extracted from a software project’s informal requirements) that fixes only expected properties but ideally says nothing about implementation issues; this is to be followed by a number of refinement steps that fix more and more details of the design, so that one finally arrives at what is often termed the design specification. The last refinement step then results in an actual implementation in a programming language.

Casl’s views express some aspect of refinement, namely that as a specification is successively refined during the development process, the model class gets smaller and smaller as more and more design decision are made, until a monomorphic design specification or program is reached. However, Casl’s views are not expressive enough for refinement, being primarily a means for naming fitting morphisms for parameterized specifications. This is because there are more aspects of refinement than just model class inclusion.

One central issue here is so-called constructor refinement [48]. This includes the basic constructions for writing implementation units that can be found in programming languages, e.g. enumeration types, algebraic datatypes (that is, free types) and recursive definitions of operations. Also, unit terms in architectural specifications can be thought of as (logic independent) constructors: they construct larger units out of smaller ones. Refinements may use these constructors, and hence the task of implementing a specification may be entirely discharged (by supplying appropriate constructs in some programming language), or may be reduced (via an architectural specification) to the implementation of smaller specifications. A first refinement language following these lines is described in [30].

A second central issue concerns behavioural refinement. Often, a refined specification does not satisfy the initial requirements literally, but only up to some sort of behavioural equivalence. E.g. if stacks are implemented as arrays-with-pointer, then two arrays-with-pointer only differing in their “junk” entries (that is, those beyond the pointer) exhibit the same behaviour in terms of the stack operations. Hence, they correspond to the same abstract stack and should be treated as being the same for the purpose of the refinement. This can be achieved e.g. by using observational equivalences between models, which are usually induced by sets of observable sorts [46].

9 CONCLUSION

Casl is a complex specification language providing both a complete formal semantics and a proof calculus for all its constructs. A central property of the design of Casl is the orthogonality between on the one hand basic specifications providing means to write theories in a specific logic, and on the other hand structured and architectural specifications, which have a logic-independent semantics. This means that the logic for basic specifications can easily be changed while keeping the rest of Casl unchanged. Indeed, Casl is actually the central language in a whole family of languages. Casl concentrates on the specification of abstract data types and (first-order) functional requirements, while some (currently still prototypical) extensions of Casl also consider the specification of higher-order functions [36, 49] and of reactive [9, 43, 44, 45] and object-oriented [3, 23] behaviour. Restrictions of Casl to sublanguages [34] make it possible to use specialized tool support.

Now that the design of Casl and its semantics have been completed and are laid out in a forthcoming two-volume book [39, 40], the next step is to put Casl into practical use. A library of basic datatypes and several case studies have been developed in Casl [1]; they show how Casl works in practice. Of course, tool support is an important issue as well. There is a Casl tool set [32] providing a parser and static analysis for the various levels of Casl. Concerning proof support for basic specifications, the Casl tool set provides several logical codings that interface Casl to existing theorem provers such as Isabelle/HOL. The tool Maya [6] provides management of proof obligations arising from Casl structured specifications. These proof obligations can be discharged by calling external theorem provers. Currently, this tool support is also being made independent of the underlying logical system, so that the orthogonality of the different levels of Casl is also reflected at the level of tools. Then programming languages (formalized as particular institutions) can also be integrated, leading to a framework and environment for formal software development.

Acknowledgements

This paper reports results of the Common Framework Initiative (CoFI); hence we thank all the contributors to CoFI, without whom it simply would not exist. This work has been partially supported by KBN grant 7T11C 002 21 and European AGILE project IST-2001-32747, and by the British-Polish Research Partnership Programme.

REFERENCES

 [1] Casl case studies. Available at http://www.pst.informatik.uni-muenchen.de/
    ~baumeist/CoFI/case.html.

[2] S. Alagi. Institutions: integrating objects, XML and databases. Information and Software Technology, 44:207–216, 2002.

[3] D. Ancona, M. Cerioli, and E. Zucca. Extending Casl by late binding. In C. Choppy, D. Bert, and P. Mosses, editors, Recent Trends in Algebraic Development Techniques, 14th International Workshop, WADT’99, Bonas, France, volume 1827 of Lecture Notes in Computer Science. Springer-Verlag, 2000.

[4] 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.

[5] E. Astesiano, H.-J. Kreowski, and B. Krieg-Brückner. Algebraic Foundations of Systems Specification. Springer, 1999.

[6] S. Autexier and T. Mossakowski. Integrating HolCasl into the development graph manager Maya. In A. Armando, editor, Frontiers of Combining Systems, 4th International Workshop, volume 2309 of Lecture Notes in Computer Science, pages 2–17. Springer-Verlag, 2002.

[7] J. Barwise and J. Etchemendy. Language, proof and logic. CSLI publications, 2002.

[8] H. Baumeister, M. Cerioli, A. Haxthausen, T. Mossakowski, P. Mosses, D. Sannella, and A. Tarlecki. Casl semantics. In P. Mosses, editor, Casl Reference Manual. [40], Part III.

[9] H. Baumeister and A. Zamulin. State-based extension of Casl. In Proceedings IFM 2000, volume 1945 of Lecture Notes in Computer Science. Springer-Verlag, 2000.

[10] M. Bidoit and R. Hennicker. On the integration of observability and reachability concepts. In M. Nielsen and U. Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 21–36. Springer, 2002.

[11] T. Borzyszkowski. Generalized interpolation in CASL. Information Processing Letters, 76/1-2:19–24, 2000.

[12] T. Borzyszkowski. Higher-order logic and theorem proving for structured specifications. In C. Choppy, D. Bert, and P. Mosses, editors, Workshop on Algebraic Development Techniques 1999, volume 1827 of LNCS, pages 401–418, 2000.

[13] T. Borzyszkowski. Logical systems for structured specifications. Theoretical Computer Science, 286:197–245, 2002.

[14] M. Cerioli, A. Haxthausen, B. Krieg-Brückner, and T. Mossakowski. Permissive subsorted partial logic in Casl. In M. Johnson, editor, Algebraic methodology and software technology: 6th international conference, AMAST 97, volume 1349 of Lecture Notes in Computer Science, pages 91–107. Springer-Verlag, 1997.

[15] C. Cirstea. Institutionalising many-sorted coalgebraic modal logic. In CMCS 2002, Electronic Notes in Theoretical Computer Science. Elsevier Science, 2002.

[16] CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible from http://www.brics.dk/

Projects/CoFI/.

[17] T. Dimitrakos and T. Maibaum. On a generalised modularisation theorem. Information Processing Letters, 74(1-2):65–71, 2000.

[18] J. L. Fiadeiro and J. F. Costa. Mirror, mirror in my hand: A duality between specifications and models of process behaviour. Mathematical Structures in Computer Science, 6(4):353–373, 1996.

[19] J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39:95–146, 1992. Predecessor in: LNCS 164, 221–256, 1984.

[20] J. A. Goguen and R. Diaconescu. Towards an algebraic semantics for the object paradigm. In RECENT trends in data type specification: workshop on specification of abstract data types: COMPASS: selected papers, number 785. Springer Verlag, Berlin, Germany, 1994.

[21] A. Haxthausen and F. Nickl. Pushouts of order-sorted algebraic specifications. In Proceedings of AMAST’96, volume 1101 of Lecture Notes in Computer Science, pages 132–147. Springer-Verlag, 1996.

[22] H. Herrlich and G. Strecker. Category Theory. Allyn and Bacon, Boston, 1973.

[23] H. Hussmann, M. Cerioli, and H. Baumeister. From UML to Casl (static part). Technical report, 2000. Technical Report of DISI - Universit di Genova, DISI-TR-00-06, Italy.

[24] C. B. Jones. Systematic Software Development Using VDM. Prentice Hall, 1990.

[25] B. Klin, P. Hoffman, A. Tarlecki, L. Schröder, and T. Mossakowski. Checking amalgamability conditions for Casl architectural specifications. In Mathematical Foundations of Computer Science, volume 2136 of LNCS, pages 451–463. Springer, 2001.

[26] CoFI Language Design Group, B. Krieg-Brückner and P.D. Mosses (eds.). Casl summary. In P. Mosses, editor, Casl Reference Manual. [40], Part I.

[27] A. Lopes and J. L. Fiadeiro. Preservation and reflection in specification. In Algebraic Methodology and Software Technology, pages 380–394, 1997.

[28] K. Meinke and J. V. Tucker, editors. Many-sorted Logic and its Applications. Wiley, 1993.

[29] J. Meseguer. General logics. In Logic Colloquium 87, pages 275–329. North Holland, 1989.

[30] T. Mossakowski. Refinement. In P. Mosses, editor, Casl Reference Manual. [40], Part V.

[31] T. Mossakowski. Colimits of order-sorted specifications. In F. Parisi Presicce, editor, Recent trends in algebraic development techniques. Proc. 12th International Workshop, volume 1376 of Lecture Notes in Computer Science, pages 316–332. Springer, 1998.

[32] T. Mossakowski. Casl: From semantics to tools. In S. Graf and M. Schwartzbach, editors, TACAS 2000, volume 1785 of Lecture Notes in Computer Science, pages 93–108. Springer-Verlag, 2000.

[33] T. Mossakowski. Specification in an arbitrary institution with symbols. In C. Choppy, D. Bert, and P. Mosses, editors, Recent Trends in Algebraic Development Techniques, 14th International Workshop, WADT’99, Bonas, France, volume 1827 of Lecture Notes in Computer Science, pages 252–270. Springer-Verlag, 2000.

[34] T. Mossakowski. Relating Casl with other specification languages: the institution level. Theoretical Computer Science, 286:367–475, 2002.

[35] T. Mossakowski, S. Autexier, and D. Hutter. Extending development graphs with hiding. In H. Hußmann, editor, Fundamental Approaches to Software Engineering, volume 2029 of Lecture Notes in Computer Science, pages 269–283. Springer-Verlag, 2001.

[36] T. Mossakowski, A. Haxthausen, and B. Krieg-Brückner. Subsorted partial higherorder logic as an extension of Casl. In C. Choppy, D. Bert, and P. Mosses, editors, Recent Trends in Algebraic Development Techniques, 14th International Workshop, WADT’99, Bonas, France, volume 1827 of Lecture Notes in Computer Science, pages 126–145. Springer-Verlag, 2000.

[37] T. Mossakowski, P. Hoffman, S. Autexier, and D. Hutter. Casl proof calculus. In P. Mosses, editor, Casl Reference Manual. [40], Part IV.

[38] P. D. Mosses. CoFI: The Common Framework Initiative for Algebraic Specification and Development. In TAPSOFT ’97, Proc. Intl. Symp. on Theory and Practice of Software Development, volume 1214 of LNCS, pages 115–137. Springer-Verlag, 1997.

[39] P. D. Mosses and M. Bidoit. Casl — the common algebraic specification language: User Manual. Lecture Notes in Computer Science. Springer. To appear.

[40] P. D. Mosses (ed.). Casl — the common algebraic specification language: Reference Manual. Lecture Notes in Computer Science. Springer. To appear.

[41] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford Univ. Press, 1990.

[42] L. Paulson. ML for the Working Programmer. Cambridge University Press, 1996. 2nd edition.

[43] G. Reggio, E. Astesiano, and C. Choppy. Casl-LTL - a Casl extension for dynamic reactive systems - summary. Technical Report of DISI - Università di Genova, DISI-TR-99-34, Italy, 2000.

[44] G. Reggio and L. Repetto. Casl-CHART: a combination of statecharts and of the algebraic specification language Casl. In Proc. AMAST 2000, volume 1816 of Lecture Notes in Computer Science. Springer Verlag, 2000.

[45] M. Roggenbach. CSP-Casl — a new integration of process algebra and algebraic specification. In Third AMAST Workshop on Algebraic Methods in Language Processing (AMiLP-3), TWLT. University of Twente, 2003. to appear.

[46] D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150–178, 1987.

[47] D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165–210, 1988.

[48] D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica, 25:233–281, 1988.

[49] L. Schröder and T. Mossakowski. HasCasl: Towards integrated specification and development of Haskell programs. In H. Kirchner and C. Reingeissen, editors, Algebraic Methodology and Software Technology, 2002, volume 2422 of Lecture Notes in Computer Science, pages 99–116. Springer-Verlag, 2002.

[50] L. Schröder, T. Mossakowski, P. Hoffman, B. Klin, and A. Tarlecki. Amalgamation in the semantics of Casl. Theoretical Computer Science, to appear.

[51] A. Sernadas, J. F. Costa, and C. Sernadas. An institution of object behaviour. In H. Ehrig and F. Orejas, editors, Recent Trends in Data Type Specification, volume 785 of Lecture Notes in Computer Science, pages 337–350. Springer-Verlag, 1994.

[52] A. Sernadas and C. Sernadas. Denotational semantics of object specification within an arbitrary temporal logic institution. Research report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 1993. Presented at IS-CORE Workshop 93.

[53] A. Sernadas, C. Sernadas, C. Caleiro, and T. Mossakowski. Categorical fibring of logics with terms and binding operators. In D. Gabbay and M. d. Rijke, editors, Frontiers of Combining Systems 2, Studies in Logic and Computation, pages 295– 316. Research Studies Press, 2000.

[54] A. Tarlecki. Abstract specification theory: an overview. In M. Broy and M. Pizka, editors, Models, Algebras, and Logics of Engineering Software, volume 191 34 T. Mossakowski, A. Haxthausen, D. Sannella, A. Tarlecki

of NATO Science Series — Computer and System Sciences, pages 43–79. IOS Press,

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

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

\frac{⊢ SP ⇒ M}{C ⊢ U : SP ⇒ C × \{U ↦ M\}}

\frac{\begin{matrix}⊢ SP_{1} ⇒ M_{1} ⊢ SP_{2} ⇒ M_{2} \\ F = \{F: M_{1} →M_{2} | for M ∈ M_{1}, F (M) _{τ} = M\} \end{matrix}}{C ⊢ U : SP_{1} ⟶^{τ} SP_{2} ⇒ C × \{U ↦ F\}}

\overline{C ⊢ U ⇒ \{E ↦ E(U ) | E ∈ C\}}

\frac{C ⊢ T ⇒ UEv for each E ∈ C, UEv(E) _{σ} ∈ Dom(E(U ))\} (∗) \begin{matrix}for each E ∈ C, there is a unique M ∈ Mod(Σ′_{T}) such that \\ M _{τ′} = UEv(E) and M _{σ′} = E(U )(UEv(E) _{σ}) \end{matrix} \} (∗∗) UEv′ = \{E ↦ M | E ∈ C, M _{τ′} = UEv(E), M _{σ′} = E(U )(UEv(E) _{σ})\}}{C ⊢ U [T fit σ] ⇒ UEv′}

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

Fig. 9. Model semantics of architectural specifications

\frac{⊢ Dcl^{∗} :: C_{v} C_{v} ⊢ T :: Σ ⟶^{i} SP′_{G} ⟵^{θ} SP_{G}}{⊢ arch spec Dcl^{∗} result T :: SP′_{G} hide i}

\frac{C_{v}^{∅} ⊢ Dcl_{1} :: (C_{v})_{1}  ⋯  (C_{v})_{n−1} ⊢ Dcl_{n} :: (C_{v})_{n}}{⊢ Dcl_{1} … Dcl_{n} :: (C_{v})_{n}}

\frac{U ∉ (Dom(P_{v}) ∪ Dom(B_{v})) ⊢ SP ⊳ Σ (Σ_{G} ⟶^{θ} Σ′_{G} ⟵^{i} Σ) is the coproduct of Σ_{G} and Σ}{(P_{v}, B_{v}, SP_{G}) ⊢ U : SP :: (P_{v}, (B_{v};θ) + \{U ↦ i\}, (SP_{G} with θ) and (SP with i))}

\frac{U ∉ (Dom(P_{v}) ∪ Dom(B_{v}))}{(P_{v}, B_{v}, SP_{G}) ⊢ U : SP_{1} ⟶^{τ} SP_{2} :: (P_{v} + \{U ↦ SP_{1} ⟶^{τ} SP_{2}\}, B_{v}, SP_{G})}

\frac{B_{v}(U ) = Σ ⟶^{i} SP_{G}}{(P_{v}, B_{v}, SP_{G}) ⊢ U :: Σ ⟶^{i} SP_{G} ⟵^{id} SP_{G}}

\frac{(P_{v}, B_{v}, SP_{G}) ⊢ T :: Σ_{T} ⟶^{i} SP′_{G} ⟵^{θ} SP_{G} P_{v}(U ) = SP ⟶^{τ} SP′ ⊢ SP ⊳ Σ ⊢ SP′ ⊳ Σ′ σ : Σ → Σ_{T} (τ′: Σ_{T} → Σ′_{T} , σ′: Σ′ → Σ′_{T}) is the pushout of (σ, τ) (τ′′: Σ′_{G} → Σ′′_{G}, i′: Σ′_{T} → Σ′′_{G}) is the pushout of (i, τ′) SP with σ;i ⇝ SP′_{G}}{(P_{v}, B_{v}, SP_{G}) ⊢ U [T fit σ] :: Σ′_{T} ⟶^{i′} (SP′_{G} with τ′′) and (SP′ with σ′;i′) ⟵^{θ;τ′′} SP_{G}}

\frac{(P_{v}, B_{v}, SP_{G}) ⊢ T_{1} :: Σ_{1} ⟶^{i_{1}} SP_{G}^{1} ⟵^{θ_{1}} SP_{G} (P_{v}, B_{v}, SP_{G}) ⊢ T_{2} :: Σ_{2} ⟶^{i_{2}} SP_{G}^{2} ⟵^{θ_{2}} SP_{G} Σ = Σ_{1} ∪ Σ_{2} with inclusions ι_{1} : Σ_{1} → Σ, ι_{2} : Σ_{2} → Σ (θ′_{2} : Σ_{G}^{1} → Σ′_{G}, θ′_{1} : Σ_{G}^{2} → Σ′_{G}) is the pushout of (θ_{1}, θ_{2}) j: Σ → Σ′_{G} satisfies ι_{1};j = i_{1};θ′_{2} and ι_{2};j = i_{2};θ′_{1}}{(P_{v}, B_{v}, SP_{G}) ⊢ T_{1} and T_{2} :: Σ_{1} ∪ Σ_{2} ⟶^{j} (SP_{G}^{1} with θ′_{2}) and (SP_{G}^{2} with θ′_{1}) ⟵^{θ_{1};θ′_{2}} SP_{G}}

Fig. 10. Verification rules

[figure: Σ; Σ_{T}; Σ′; Σ′_{T}; σ; τ; τ′; σ′; Σ_{G}; Σ′_{G}; Σ′′_{G}; θ; τ′′; i; i′; Σ_{G}; Σ_{G}^{1}; Σ_{G}^{2}; Σ_{1}; Σ_{2}; Σ_{1} ∪ Σ_{2}; Σ′_{G}; θ_{2}; θ_{1}; i_{1}; i_{2}; ι_{1}; ι_{2}; j; θ′_{2}; θ′_{1}]

Fig. 11. Diagrams for unit application and amalgamation