Logical foundations of cafeOBJ.
This paper surveys the logical and mathematical foundations of CafeOBJ, which is a successor of the famous algebraic specification language OBJ but adds to it several new primitive paradigms such as behavioural concurrent specification and rewriting logic.We first give a concise overview of CafeOBJ. Then we focus on the actual logical foundations of the language at two different levels: basic specification and structured specification, including also the definition of the CafeOBJ institution. We survey some novel or more classical theoretical concepts supporting the logical foundations of CafeOBJ, pointing out the main results but without giving proofs and without discussing all mathematical details. Novel theoretical concepts include the coherent hidden algebra formalism and its combination with rewriting logic, and Grothendieck (or fibred) institutions. However, for proofs and for some of the mathematical details not discussed here we give pointers to relevant publications.The logical foundations of CafeOBJ are structured by the concept of institution. Moreover, the design of CafeOBJ emerged from its logical foundations, and institution concepts played a crucial rle in structuring the language design.
Introduction
CafeOBJ is an executable industrial strength algebraic specification language which
is a modern successor of OBJ and incorporating several new algebraic specification
paradigms. Its definition is given in [12]. CafeOBJ is intended to be mainly used
for system specification, formal verification of specifications, rapid prototyping,
programming, etc. Here is a brief overview of its most important features.
On leave from the Institute of Mathematics of the Romanian Academy.
Preprint submitted to Elsevier Preprint 26 February 2000
Equational Specification and Programming.
This is inherited from OBJ [27, 17] and constitutes the basis of the language, the
other features being somehow built on top of it. As with OBJ, CafeOBJ is executable
(by term rewriting), which gives an elegant declarative way of functional
programming, often referred as algebraic programming. 3 As with OBJ, CafeOBJ
also permits equational specification modulo several equational theories such as
associativity, commutativity, identity, idempotence, and combinations between all
these. This feature is reflected at the execution level by term rewriting modulo such
equational theories.
Behavioural Specification.
Behavioural specification [21, 22, 13, 29] provides a novel generalisation of ordinary
algebraic specification. Behavioural specification characterises how objects
(and systems) behave, not how they are implemented. This new form of abstraction
can be very powerful in the specification and verification of software systems since
it naturally embeds other useful paradigms such as concurrency, object-orientation,
constraints, nondeterminism, etc. (see [22] for details). Behavioural abstraction is
achieved by using specification with hidden sorts and a behavioural concept of satisfaction
based on the idea of indistinguishability of states that are observationally
the same, which also generalises process algebra and transition systems (see [22]).
CafeOBJ behavioural specification paradigm is based on coherent hidden algebra
(abbreviated 'CHA') of [13], which is both an simplification and extension of classical
hidden algebra of [22] in several directions, most notably allowing operations
with multiple hidden sorts in the arity. Coherent hidden algebra comes very close
to the "observational logic" of Bidoit and Hennicker [29].
CafeOBJ directly supports behavioural specification and its proof theory through
special language constructs, such as
hidden sorts (for states of systems),
behavioural operations (for direct "actions" and "observations" on states of sys-
tems),
behavioural coherence declarations for (non-behavioural) operations (which may
be either derived (indirect) "observations" or "constructors" on states of sys-
tems), and
behavioural axioms (stating behavioural satisfaction).
The advanced coinduction proof method receives support in CafeOBJ via a default
coinduction relation (denoted =*=). In CafeOBJ, coinduction can
be used either in the classical hidden algebra sense [22] for proving behavioural
Please notice that although this paradigm may be used as programming, this aspect is
still secondary to its specification side.
equivalence of states of objects, or for proving behavioural transitions (which appear
when applying behavioural abstraction to rewriting logic). 4
Besides language constructs, CafeOBJ supports behavioural specification and verification
by several methodologies. 5 CafeOBJ currently highlights a methodology
for concurrent object composition which features high reusability not only of
specification code but also of verifications [12, 30]. Behavioural specification in
CafeOBJ may also be effectively used as an object-oriented (state-oriented) alternative
for classical data-oriented specifications. Experiments seem to indicate that
an object-oriented style of specification even of basic data types (such as sets, lists,
etc.) may lead to higher simplicity of code and drastic simplification of verification
process [12].
Behavioural specification is reflected at the execution level by the concept of behavioural
rewriting [12, 13] which refines ordinary rewriting with a condition ensuring
the correctness of the use of behavioural equations in proving strict equalities

Rewriting Logic Specification.
Rewriting logic specification in CafeOBJ is based on a simplified version of Mese-
guer's rewriting logic (abbreviated as `RWL') [32] specification framework for concurrent
systems which gives a non-trivial extension of traditional algebraic specification
towards concurrency. RWL incorporates many different models of concurrency
in a natural, simple, and elegant way, thus giving CafeOBJ a wide range of
applications. Unlike Maude [2], the current CafeOBJ design does not fully support
labelled RWL which permits full reasoning about multiple transitions between
states (or system configurations), but provides proof support for reasoning about the
existence of transitions between states (or configurations) of concurrent systems via
a built-in predicate (denoted ==>) with dynamic definition encoding both the proof
theory of RWL and the user defined transitions (rules) into equational logic.
From a methodological perspective, CafeOBJ develops the use of RWL transitions
for specifying and verifying the properties of declarative encoding of algorithms
(see [12]) as well as for specifying and verifying transition systems.
4 However, until the time this paper was written, the latter has not been yet explored suffi-
ciently, especially practically.
5 This is still an open research topic, the current methodologies may be developed further
and new methodologies may be added in the future.
Module System.
The principles of the CafeOBJ module system are inherited from OBJ which
builds on ideas first realized in the language Clear [1], most notably institutions
[19, 15]. CafeOBJ module system features
several kinds of imports,
sharing for multiple imports,
parameterised programming allowing
multiple parameters,
views for parameter instantiation,
integration of CafeOBJ specifications with executable code in a lower level
language
module expressions.
However, the concrete design of the language revise the OBJ view on importation
modes and parameters [12].
Type System and Partiality.
CafeOBJ has a type system that allows subtypes based on order sorted algebra
(abbreviated 'OSA') [25, 20]. This provides a mathematically rigorous form of
runtime type checking and error handling, giving CafeOBJ a syntactic flexibility
comparable to that of untyped languages, while preserving all the advantages of
strong typing.
At this moment the concrete order sortedness formalism is still open at least at the
level of the language definition. CafeOBJ does not directly do partial operations
but rather handles them by using error sorts and a sort membership predicate in the
style of membership equational logic (abbreviated 'MEL') [33]. The semantics of
specifications with partial operations is given by MEL.
Logical semantics.
CafeOBJ is a declarative language with firm mathematical and logical foundations
in the same way as other OBJ-family languages (OBJ, Eqlog [23, 4], FOOPS [24],
Maude [32]) are. The mathematical semantics of CafeOBJ is based on state-of-the-
art algebraic specification concepts and results, and is strongly based on category
theory and the theory of institutions [19, 11, 9, 15]. The following are the principles
governing the logical and mathematical foundations of CafeOBJ:
P1. there is an underlying logic 6 in which all basic constructs and features of
6 Here "logic" should be understood in the modern relativistic sense of "institution" which
the language can be rigorously explained.
P2. provide an integrated, cohesive, and unitary approach to the semantics
of specification in-the-small and in-the-large.
P3. develop all ingredients (concepts, results, etc.) at the highest appropriate
level of abstraction.
CafeOBJ is a multi-paradigm language. Each of the main paradigms implemented
in CafeOBJ is rigorously based on some underlying logic; the paradigms resulting
from various combinations are based on the combination of logics. The structure of
these logics is shown by the following CafeOBJ cube, where the full arrows mean
embedding between the logics, which correspond to institution embeddings (i.e., a
strong form of institution morphisms of [19, 15]) (the orientation of arrows goes
from "more complex" to "less complex" logics).
HA
MSA RWL
OSRWL
HOSA
OSA
=many
rewriting logic
The mathematical structure represented by this cube is that of an indexed institution
[11]. The CafeOBJ institution is a Grothendieck (or fibred) institution [11]
obtained by applying a Grothendieck construction to this cube (i.e., the indexed
institution). Note that by employing other logical-based paradigms the CafeOBJ
cube may be thought as a hyper-cube (see [12] for details).
1.1 Summary of the paper
The first part of this paper is dedicated to the foundations of basic specifications.
The main topic of this part is the definition of HOSRWL, the hidden order sorted
rewriting logic institution, which embeds all other institutions of the CafeOBJ
cube. In this way, the HOSRWL institution contains the mathematical foundations
for all basic specification CafeOBJ constructs.
The second part of the paper presents the novel concept of Grothendieck institution
provides a mathematical definition for a logic (see [19]) rather than in the more classical
sense.
(developed by [11]) which constructs the CafeOBJ institution from the CafeOBJ
cube.
The last section contains the definitions of the main mathematical concepts for
structuring specification in CafeOBJ.
The main concepts of the logical foundations of CafeOBJ are illustrated with several
examples, including CafeOBJ code. We assume familiarity with CafeOBJ
including its syntax and semantics (see [12] or several papers such as [14]).
Terminology and Notations
This work assumes some familiarity with basic general algebra (in its many-sorted
and order-sorted form) and category theory. Relevant background in general algebra
can be found in [18, 26, 34] for the many-sorted version, and in [25, 20] for
the order-sorted version. For category theory we generally use the same notations
and terminology as Mac Lane [31], except that composition is denoted by ";" and
written in the diagrammatic order. The application of functions (functors) to arguments
may be written either normally using parentheses, or else in diagrammatic
order without parentheses, or, more rarely, by using sub-scripts or super-scripts.
The category of sets is denoted as Set, and the category of categories 7 as C at . The
opposite of a category C is denoted by C op . The class of objects of a category C is
denoted by jC j; also the set of arrows in C having the object a as source and the
object b as target is denoted as C (a;b).
Indexed categories [35] play an important r"ole in for this work. [36] constitutes a
good reference for indexed categories and their applications to algebraic specifica-
tion. An indexed category [36] is a sometimes we denote
for an index i 2 jIj and B(u) as B u for an index morphism u 2 I.
The following 'flattening' construction providing the canonical fibration associated
to an indexed category is known under the name of the Grothendieck construc-
tion) and plays an important r"ole in mathematics and in particular in this paper.
Given an indexed category be the Grothendieck category having
objects and hu; ji :
arrows. The composition of arrows in B ] is defined
by hu; ji;hu
7 We steer clear of any foundational problem related to the "category of all categories";
several solutions can be found in the literature, see, for example [31].
2 Foundations of Basic Specifications
At this level, semantics of CafeOBJ is concerned with the semantics of collections
of specification statements. CafeOBJ modules can be flattened to such basic specifications
by an obvious induction process on the module composition structure. In
CafeOBJ we can have several kinds of specifications, the basic kinds corresponding
to the basic CafeOBJ specification/programming paradigms:
equational specifications,
rewriting specifications,
behavioural specifications, and
behavioural rewriting specifications.
The membership of a basic specification to a certain class is determined by the
CafeOBJ convention that each basic specification should be regarded as implementing
the simplest possible combination of paradigms resulting from its syntactic
content.
2.1 Loose and Tight Denotation
The key concept of specification in-the-small is the satisfaction relation between
the models and the sentences of a given specification, which is also the key notion
of the abstract concept of institution. Each kind of specification has its own concept
of satisfaction, and Section 2.2 surveys them briefly.
Each class of basic specifications has an underlying logic in the CafeOBJ cube.
Specifications can be regarded as finite sets of sentences in the underlying logic.
This enables us to formulate the principle of semantics of CafeOBJ specification
in-the-small:
Each basic specification determines a theory in the corresponding
institution. The denotation [[SP]] of a basic specification SP is the class of
models MOD(T SP ) of its corresponding theory T SP if loose, and it is the
initial model 0 T SP of the theory, if tight.
A basic specification can have either loose or initial denotation, and this can be directly
specified by the user. CafeOBJ does not directly implement final semantics,
however final models play an important r"ole for the loose semantics of behavioural
specifications (see [13, 8]).
Initial model semantics applies only to non-behavioural specification, and is supported
by the following result:
Theorem 1 Let T be a theory in either MSA, OSA, RWL, or OSRWL. Then the
initial model 0 T exists.
This very important result appears in various variants and can be regarded as a
classic of algebraic specification theory. The reader may wish to consult [26] for
MSA, [25, 20] for OSA, [32] for RWL, and although, up to our knowledge, the
result has not yet been published, it is also valid for OSRWL.
Because of the importance of the construction of the initial model we briefly recall
it here. Let S be the signature of the theory consisting of a set S of sorts (which is a
partial order in the order-sorted case) and a ranked (by S  ) set of operation symbols
(possibly overloaded). The S-sorted set T S of S-terms is the least S-sorted set closed
under:
- each constant is a S-term (denoted S [];s
ng.
The operations in S can be interpreted on T S in the obvious manner, thus making
it into a S-algebra 0 S . If T is equational, then its ground part is a congruence  T
on 0 S . Then 0 T is the quotient whose carriers are equivalence classes of
S-terms under  T . If T is a pure rewriting theory then 0 T is a rewriting logic model
whose carriers (0 T ) s are categories with S-terms as objects and concurrent rewrite
sequences (using the rules of T ) as arrows. Finally, rewrite theories including equations
require the combination between the above two constructions.
Example 2 Consider the following CafeOBJ specification of non-deterministic
natural numbers:
mod! NNAT {
protecting(NAT)
trans M:Nat | N:Nat => M .
trans M:Nat | N:Nat => N .
The denotation of NNat is initial and consists [of the isomorphism class] of one
model, 0 NNat
, the initial model. The main carrier of 0 NNat
is a category which has
non-empty lists of natural numbers as objects and deletion sequences as arrows.
| gets interpreted as a functor which concatenates lists of numbers on objects,
and compose in parallel ("horizontally") deletion sequences.
2.2 Hidden Order Sorted Rewriting Logic Institution
We devote this section to the definition of the HOSRWL institution (defined for
the first time in [8] in the many sorted version) which embeds all CafeOBJ cube
institutions. We recall here that the behavioural specification part of HOSRWL is
based on the 'coherent hidden algebra' of [13]. The deep understanding of HOS-
RWL requires further reading on its main components ([32] for RWL and [13] for
CHA) as well as their integration [8].
Signatures
Definition 3 A HOSRWL signature is a tuple (H;V;;S;S b ), where
(H;) and (V;) are disjoint partial ordered sets of hidden sorts and visible
respectively,
S is a (H [V;)-order-sorted signature,
is a subset of behavioural operations such that s 2 S b
w;s has exactly one
hidden sort in w.
Notice that we may simplify the notation (H;V;;S;S b ) to just (H;V;;S) , or
just S, when no confusion is possible.
From a methodological perspective, the operations in S b have object-oriented mean-
w;s is thought as an action (or "method" in a more classical jargon) on the
space (type) of states if s is hidden, and thought as observation (or "attribute" in
a more classical jargon) if s is visible. The last condition says that the actions and
observations act on (states of) single objects.
is an order-sorted signature morphism (H
such that
hidden sorts h;h
These conditions say that hidden sorted signature morphisms preserve visibility and
invisibility for both sorts and operations, and the S 0 b  F(S b ) inclusion together
with (M3) expresses the encapsulation of classes (in the sense that no new actions
(methods) or observations (attributes) can be defined on an imported class) 8 . How-
ever, these conditions apply only to the case when signature morphisms are used as
8 Without it the Satisfaction Condition fails, for more details on the logical and computational
relevance of this condition see [21].
module imports (the so-called horizontal signature morphisms); when they model
specification refinement this condition might be dropped (this case is called vertical
signature morphism).
Proposition 5 HOSRWL signatures and signature morphisms (with the obvious
composition) form a category denoted as Sign
HOSRWL .
Sentences
In HOSRWL there are several kinds of sentences inherited from the various CafeOBJ
cube institutions.
Definition 6 Consider a HOSRWL signature (H;V;;S;S b ). Then a (strict) equation
is a sentence of the form
where X is a (H [V )-sorted set of variables, t; t 0 are S-terms with variables X , and
C is a Boolean(-sorted) S-term,
a behavioural equation is a sentence of the form
a (strict) transition is a sentence of the form
and a behavioural transition is a sentence of the form
have the same meaning as for strict equations.
All these sentences are here defined in the conditional form. If the condition is
missing (which is equivalent to saying it is always true), then we get the unconditional
versions of sentences. Notice also that our approach to conditional sentences
is slightly different from the literature in the sense that the condition is a Boolean
term rather than a finite conjunction of formul. Our approach is more faithful to
the concrete level of CafeOBJ and is also more general. This means that a finite
conjunction of formul can be translated to a Boolean term by using some special
semantic predicates (such as == for semantics equality and ==> for the semantic
transition relation, in CafeOBJ). We do not discuss here the full details of this ap-
proach, we only further mention that the full rigorous treatment of such conditions
can be achieved within the so-called constraint logic [10], which can however be
regarded as a special case of an abstract categorical form of plain equational logic
[5, 4,
Equational attributes such as associativity (A), commutativity (C), identity (I), or
idempotence (Z) are just special cases of strict equations. However, the behavioural
part of HOSRWL has another special attribute called behavioural coherence [12,
13] which is regarded as a sentence:
Definition 7 Let (H;V;;S;S b ) be a signature. Then
s coherent
is a behavioural coherence declaration for s, where s is any operation S.
Definition 8 Given a signature morphism
the translation of sentences is defined by replacing all operation symbols from S
with the corresponding symbols (via F) from S 0 and by re-arranging the sort of the
variables involved accordingly to the sort mapping given by F.
Fact 9 If we denote the set of sentences of a signature (H;V;;S;S b ) by
Sen HOSRWL (H;V;;S;S b ) and the sentence translation corresponding to a signature
morphism F by Sen HOSRWL (F), then this gets a sentence functor
Models
Models of HOSRWL are rewrite models [32] which are (algebraic) interpretations
of the signatures into C at (the category of small categories) rather than in Set (the
category of small sets) as in the case of ordinary algebras. Thus, ordinary algebras
can be regarded as a special case of rewrite models with discrete carriers.
Given a HOSRWL signature (H;V;;S;S b ), a HOSRWL model M
interprets:
each sort s as a small category M s and each subsort relation s < s 0 as sub-category
relation
, and
each operation s 2 S w;s as a functor
Notice that each S-term by evaluating it
for each assignment of the variables occurring in t with objects or arrows from the
corresponding carriers of M.
Model homomorphisms in HOSRWL follow an idea of [29] by refining the ordinary
concept of model morphism and reforming the hidden algebra [21, 22] homomorphisms
by taking adequate care of the behavioural structure of models. We need
first to define the concept of behavioural equivalence.
Definition 11 Recall that a S-context c[z] is any S-term c with a marked variable
z occurring only once in c. A context c[z] is behavioural iff all operations above z
are behavioural.
Given a model M, two elements (of the same sort s; they can be either both objects
or both arrows) a and a 0 are called behaviourally equivalent, denoted a  s a 0 (or
just a  a 0 ) iff 9
for all visible behavioural contexts c.
Remark that the behavioural equivalence is a (H [V )-sorted equivalence relation,
and on the visible sorts the behavioural equivalence coincides with the (strict)
equality relation.
Now we are ready to give the definition of model homomorphism in HOSRWL.
between models of a signature (H;V;
between the carriers such that
(for each sort s):
for all a 2 M s there exists a
s (a and a 0 can be either both arrows or both
elements) such that a h s a 0 ,
for all a 2 M s , if a h a 0 then (a h b 0 if and only if a 0  b 0 ),
for all a;b 2 M s and a
s , if a h a 0 and a  b then b h a 0 , and
for each operation s2S w;s , for all a 2M w and a 0 2M 0
w , a h w a 0 implies M s (a) h w M 0
(component-wise).
Notice that when there are no hidden sorts (i.e., we are in some non-behavioural part
of HOSRWL), this concept of model homomorphism coincides with the rewriting
model homomorphism.
For a given signature (H;V;;S), we denote its category of models by MOD HOSRWL .
Notice that any signature morphism
a model reduct
in the usual way (by renaming the sorts of the carriers and the interpretations
of the operations accordingly to the mapping of sorts and operations given by
F). Therefore we have a contravariant model functor
at op .
9 Notice that this equality means an equality between functions M
, where
This is a relation between the sets of objects together with a relation between the sets of
arrows, such that this couple of relations commute with the domain functions, codomain
functions, and arrow composition functions.
Satisfaction
The satisfaction relation between sentences and models is the crucial concept of an
institution (see Definition 19).
Consider a model M of a signature (H;V;;S;S b ). Then M satisfies
an equation, i.e., M only if
for all valuations (Notice that this applies both for objects and arrows,
since valuations may map variables either to objects or arrows.)
M satisfies a behavioural equation, i.e., M only if
for all valuations
M satisfies a transition, i.e., M only if for each
"object there is an arrow a
M C (q) is true such that for all "arrow we have a
a q
M satisfies a behavioural transition, i.e., M only if
for each appropriate visible behavioural context c and for each "object valuation"
there is an arrow a c
true such that for all "arrow we have a c
Finally, M satisfies a coherence declaration, i.e., M coherent ), if and only
if s preserves the behavioural equivalence on M, i.e.,
for all a;a 0 2 Mw .
11 I.e. a is a natural transformation.
Notice that the behavioural coherence of both the behavioural operations and of
operations of a visible rank is trivially satisfied.
Example 14 Consider the following CafeOBJ behavioural specification of non-deterministic
naturals:
mod* NNAT-HSA {
protecting(NAT)
*[ NNat ]*
vars
vars
or S2 -> N .
Notice that for all models M of NNAT-HSA,
This situation when the operations which are neither behavioural or a data type
operations (i.e. with visible rank) are automatically coherent is rather natural and
occurs very often in practice, and this corresponds to the so-called coherence conservative
methodology of [13].
The definition of the satisfaction relation between sentences and models completes
the construction of the HOSRWL institution:
Theorem 15 (Sign HOSRWL ; Sen HOSRWL ; MOD HOSRWL ; j=) is an institution.
For the definition of institution see Definition 19 given below. We omit here the
proof of this result which is rather long and tedious and follows the same pattern as
proofs of similar results, also reusing some of them (such as the proof that RWL is
an institution).
At the end of the presentation of the HOSRWL institution we give a brief example
of a CafeOBJ specification in HOSRWL:
Example Consider a behavioural specification of sets of non-determinstic naturals

mod* SETS {
protecting(NNAT)
vars
vars S
or (E in S) .
in S1) or (E in S2) .
in S1) and (E in S2) .
not (E in S1) .
where NNAT is the RWL specification of non-determinstic naturals of Example
2. Notice that each model of SETS satisfies the usual set theory rules (such as
commutativity and associativity of union and intersection, De Morgan laws, etc.)
only behaviourally, not necessarily in the strict sense. For example, the following
De Morgan behavioural rule
is a consequence of the specification SETS. Also, the following behavioural tran-
sition
btrans add(M | N, S) => add(M, S) .
is a consequence of SETS too.
Specifications in full HOSRWL naturally occurs in the case of a behavioural specification
using concurrent (RWL) data types. However the practical significance of
full HOSRWL is still little understood. The real importance of the HOSRWL institution
is its initiality in the CafeOBJ cube. We will see below that the existence
of all possible combinations between the main logics/institutions of CafeOBJ is
crucial for the good properties of the CafeOBJ institution.
2.3 Operational vs. Logical Semantics
The operational semantics underlies the execution of specifications or programs.
As with OBJ, the CafeOBJ operational semantics is based on rewriting, which in
the case of proofs is used without directly involving the user defined transitions
(rules) but rather involving them via the built-in semantic transition predicate ==>.
For executions of concurrent systems specified in rewriting logic, CafeOBJ uses
both the user-defined transitions and equations.
Since rewriting is a very well know topic in algebraic specification, we do not insist
here on the standard aspects of rewriting. However, the operational semantics of
behavioural specification requires a more sophisticated notion of rewriting which
takes special care of the use of behavioural sentences during the rewriting process,
which we call behavioural rewriting [12, 13]:
Definition 17 Given a HOSRWL signature S and a S-algebra A, a behaviourally
coherent context for A is any S-context c[z] such that all operations above 12 the
marked variable z are either behavioural or behaviourally coherent for A.
Notice that any behavioural context is also behaviourally coherent.
The following Proposition from [13] ensures the soundness of behavioural rewriting

Proposition Consider a HOSRWL signature S, a set E of S-sentences regarded
as a TRS (i.e. term rewriting system), and a S-algebra A satisfying the sentences
in E. If t 0 is a ground term and for any rewrite step t which uses a behavioural
equation from E, the rewrite context has a visible behaviourally coherent
sub-context for A, then A
If the rewrite context is behaviourally
coherent for A, then A
The completeness of the operational semantics with respect to the logical semantics
is a two-layer completeness going via the important intermediate level of the proof
calculi.
Denotational
Proof
Calculus
Operational
The completeness of the proof calculus is one of the most important class of results
in algebraic specification, for equational logic we refer to [25], and for rewriting
logic to [32]. In the case of rewriting logic the relationship between the proof calculus
and rewriting is very intimate, but for equational logic the completeness of
rewriting can be found, among other many places, in [18, 7].
Notice that hidden logics of the CafeOBJ cube do not admit a complete (finitary)
proof calculus. However, advanced proof techniques support the verification process
in the case of behavioural specifications, most notably the hidden coinduction
method (see [22] for the original definition, [12, 13] for its realization in CafeOBJ,
and [6] for the details for the case of proving behavioural transitions).
12 Meaning that z is in the subterm determined by the operation.
3 The CafeOBJ Institution
In this section we define the CafeOBJ institution, which is a Grothendieck construction
on the CafeOBJ cube. The Grothendieck construction for institutions
was first introduced by [11] and generalises the famous Grothendieck construction
for categories [28]. The essence of this Grothendieck construction is that it constructs
a 'disjoint sum' of all institutions of the CafeOBJ cube, also introducing
theory morphisms across the institution embeddings of the CafeOBJ cube. Such
extra theory morphisms were first studied in [9]. However, one advantage of the
Grothendieck institutions is that they treat the extra theory morphisms as ordinary
theory morphisms, thus leading to a conceptual simplification with respect to [9].
The reader might wonder why one cannot live with HOSRWL only (which embeds
all the CafeOBJ cube institutions) and we still need a Grothendieck construction
on the CafeOBJ cube. The reason for this is that the combination of
logics/institutions realized by HOSRWL collapses crucial semantic information,
therefore a more refined construction which preserves the identity of each of the
CafeOBJ cube institutions, but yet allowing a concept of theory morphism across
the institution embeddings, is necessary. For example, in the case of specifications
with loose semantics without a RWL component, the carriers of the models of
these specifications should be sets rather than categories, which is not possible
in HOSRWL. Therefore, such specifications should be given semantics within the
appropriate institution of the CafeOBJ cube rather than in HOSRWL. Example 36
illustrates this argument.
3.1 Institutions
We now recall from [19] the definitions of the main institution concepts:
Definition 19 An institution consists of
(1) a category Sign, whose objects are called signatures,
(2) a functor Sen : Sign!Set, giving for each signature a set whose elements are
called sentences over that signature,
(3) a functor MOD : Sign op ! C at giving for each signature S a category whose
objects are called S-models, and whose arrows are called S-(model) mor-
phisms, and
a relation for each S2 jSignj, called S-satisfaction,
such that for each morphism j in Sign, the satisfaction condition
holds for each m 0 2 jMOD(S 0 )j and e 2 Sen(S). We may denote the reduct functor
MOD(j) by  j and the sentence translation Sen(j) by j( ).
be an institution. For any signature S
the closure of a set E of S-sentences is . (S;E) is a theory if
and only if E is closed, i.e.,
A theory morphism
that j(E)  E 0 . Let Th() denote the category of all theories in .
For any institution , the model functor MOD extends from the category of its
signatures Sign to the category of its theories Th(), by mapping a theory (S;E) to
the full subcategory MOD(S;E) of MOD(S) formed by the S-models which satisfy
liberal if and only if the
reduct functor
The institution  is liberal if and only if each theory morphism is liberal.
Definition 22 An institution exact if and only if the
model functor MOD : Sign op ! C at preserves finite limits.  is semi-exact if and
only if MOD preserves only pullbacks.
Definition 23 Let  and  0 be institutions. Then an institution homomorphism
consists of
(1) a
(2) a natural transformation a
(3) a natural transformation
such that the following satisfaction condition holds
for any S 0 -model m 0 from  0 and any S 0 F-sentence e from .
Fact 24 Institutions and institution homomorphisms form a category denoted as
Ins.
The following properties of institution homomorphisms were defined in [11] and
play an important r"ole for Grothendieck institutions:
Definition 25 An institution homomorphism
means that M S-model M that satisfies all sentences in E .
an embedding iff F admits a left-adjoint F (with unit z); an institution embedding
is denoted as
liberal iff b S 0
has a left-adjoint b S 0
for each S 0 2 jSign 0 j.
An institution embedding exact if and only if the square
below is a pullback
MOD(SFF)
MOD(Sz)
(jF)
signature morphism in .
3.2 Indexed and Grothendieck Institutions
The following definition from [11] generalises the concept of indexed category [36]
to institutions.
Definition 26 An indexed institution  is a functor  : I op ! Ins.
The CafeOBJ cube is an indexed institution where the index category I is the
8-element lattice corresponding to the cube (i.e., the elements of the lattice correspond
to the nodes of the cube and the partial order is given by the arrows of the
cube).
Definition 27 The Grothendieck institution  ] of an indexed institution  : I op !
Ins has
(1) the Grothendieck category Sign ] as its category of signatures, where Sign: I op !
C at is the indexed category of signatures of the indexed institution ,
C at as its model functor, where
for each index i 2 jIj and signature S 2 jSign i j,
and
its sentence functor, where
for each index i 2 jIj and signature S 2 jSign i j, and
for each
S e for each index
For the category minded readers we mention that [11] gives a higher level characterisation
of the Grothendieck institution as a lax colimit in the 2-category Ins (with
institutions as objects, institution homomorphisms as 1-cells, and institution modifications
as 2-cells; see [11] for details) of the corresponding indexed institution.
This means that Grothendieck institutions are internal Grothendieck objects 14 in
Ins in the same way as Grothendieck categories are Grothendieck objects in C at .
For the fibred category minded readers, in [11] we also introduce the alternative formulation
of fibred institution and show that there is a natural equivalence between
split fibred institutions and Grothendieck institutions.
We would also like to mention that the concept of extra theory morphism [9] across
an institution homomorphism  0 ! (with all its subsequent concepts) is recuper-
ated as an ordinary theory morphism in the Grothendieck institution of the indexed
institution given by the homomorphism  0 !  (i.e., which has  !  as its index
category).
Now we are ready to define the institution of CafeOBJ:
Definition 28 The CafeOBJ institution is the Grothendieck institution of the CafeOBJ
cube.
3.3 Properties of the CafeOBJ Institution
In this section, we briefly study the most important institutional properties of the
CafeOBJ institution: existence of theory colimits, liberality (i.e. free construc-
tions), and exactness (i.e. model amalgamation).
The institution homomorphisms of the CafeOBJ cube are all embeddings; this
makes the CafeOBJ cube an embedding-indexed institution (cf. [11]). As we will
see below, this property of the CafeOBJ cube plays an important r"ole for the properties
of the CafeOBJ institution.
Theory Colimits.
The existence of theory colimits is crucial for any module system in the Clear-OBJ
tradition. Let us recall the following result from [11]:
14 From [11], a Grothendieck object in a 2-category is a lax colimit of a 1-functor to that
2-category.
Theorem 29 Let  : I op ! Ins be an embedding-indexed institution such that I is
J-cocomplete for a small category J. Then the category of theories Th(
) of the
Grothendieck institution  ] has J-colimits if and only if the category of signatures
Sign i is J-cocomplete for each index i 2 jIj.
Corollary The category of theories of the CafeOBJ institution is small cocomplete

Notice that the fact that the lattice of institutions of the CafeOBJ cube is complete
(as a lattice) means exactly that the index category of the CafeOBJ cube is
(small) cocomplete, which is a precondition for the existence of theory colimits in
the CafeOBJ institution. In the absence of the combinations of logics/institution
of the CafeOBJ cube (such as HOSRWL), the possibility of theory colimits in the
CafeOBJ institution would have been lost.
Liberality.
Liberality is a desirable property in relation to initial denotations for structured
specifications. In the case of loose denotations liberality is not necessary. Since
the behavioural specification paradigm involves only loose denotations, in the case
of the CafeOBJ institution, we are therefore interested in liberality only for the
non-behavioural theories. Recall the following result from [11]:
Theorem 31 The Grothendieck institution  ] of an indexed institution  : I op !
Ins is liberal if and only if  i is liberal for each index i 2 jIj and each institution
homomorphism  u is liberal for each index morphism u 2 I.
Corollary In the CafeOBJ institution, each theory morphism between non-
behavioural theories is liberal.
Notice that this corollary is obtained from the theorem above by restricting the
index category to the non-behavioural square of the CafeOBJ cube, and from the
corresponding liberality results for equational and rewriting logics.
Exactness.
Firstly, let us extend the usual exactness results for equational and rewriting logics
to the CafeOBJ cube:
Proposition 33 All institutions of the CafeOBJ cube are semi-exact.
As shown in [9] and [11], in practice exactness is a property hardly achieved at the
global level by the Grothendieck institutions. In [11] we give a necessary and sufficient
set of conditions for (semi-)exactness of Grothendieck institutions. One of
them is the exactness of the institution embeddings, which fails for the embeddings
from the non-RWL institutions into the RWL institutions of the CafeOBJ cube. In
the absence of a desired global exactness property for the CafeOBJ institution, we
need a set of sufficient conditions for exactness for practically significant particular
cases. In [9] we formulate a set of such sufficient conditions, but this problem is
still open.
4 Foundations of Structured Specifications
In this section we survey the mathematical foundations of the CafeOBJ module
composition system. CafeOBJ module composition system follows the principles
of the OBJ module system which are inherited from earlier work on Clear [1].
Consequently, CafeOBJ module system is institution-independent (i.e., can be developed
at the abstract level of institutions) in the style of [15]. In the actual case
of CafeOBJ, the institution-independent semantics is instantiated to the CafeOBJ
institution. The following principle governs the semantics of programming in-the-
large in CafeOBJ:
(L) For each structured specification we consider the theory corresponding
to its flattening to a basic specification. The structuring constructs are
modelled as theory morphisms between these corresponding theories.
The denotation [[SP]] of a structured specification is determined from the
denotations of the components recursively via the structuring constructs
involved.
The general structuring mechanism is constituted by module expressions, which
are iterations of several basic structuring operations, such as (multiple) imports,
parameters, instantiation of parameters by views, translations, etc.
4.1 Module Imports
Module imports constitute the most primitive structuring construct in any module
composition system. The concept of module import in the institution-independent
semantics of CafeOBJ is based on the mathematical notion of inclusion system.
Module imports are modeled as inclusion theory morphisms between the
theories corresponding to flattening the imported and the importing modules

Inclusion systems where first defined by [15] for the institution-independent study
of structuring specifications. Weak inclusion systems were introduced in [3], and
they constitute a simplification of the original definition of inclusion systems of
[15]. We recall the definition of inclusion systems:
Definition 34 hI ; Ei is a weak inclusion system for a category C if I and E are
two sub-categories with jI
(1) I is a partial order, and
(2) every arrow f in C can be factored uniquely as
The arrows of I are called inclusions, and the arrows of E are called
tions. 15 The domain (source) of the inclusion i in the factorisation of f is called
the image of f and denoted as Im( f ). An injection is a composition between an
inclusion and an isomorphism.
A weak inclusion system hI ; Ei is an inclusion system iff I has finite least upper
bounds (denoted +) and all surjections are epics (see [15]).
The inclusion system for the category of theories of the CafeOBJ institution is obtained
by lifting the inclusion system for its category of signatures (see [15, 3]). The
inclusion system for the category of signatures is obtained from the canonical
inclusion systems of the categories of signatures of the CafeOBJ cube institutions
by using the following result from [11] (which appeared previously in a slightly
different form in [9]):
Theorem C at be an indexed category such that
I has a weak inclusion system hI I
has a weak inclusion system hI
preserves inclusions for each inclusion index morphism u 2 I I , and
preserves inclusions and surjections and lifts inclusions uniquely for each
surjection index morphism
Then, the Grothendieck category B ] has an inclusion system hI B
is
inclusion iff both u and j are inclusions, and
surjection iff both u and j are surjections.
In the case of the CafeOBJ institution, this result is applied for the indexed category
of signatures of the CafeOBJ cube.
Example 36 Consider the following module import:
mod* TRIV { [ Elt
15 Surjections of some weak inclusion systems need not necessarily be surjective in the
ordinary sense.
mod* NTRIV {
protecting(TRIV)
trans M:Elt | N:Elt => M .
trans M:Elt | N:Elt => N .
Module TRIV gets a MSA loose theory, which has all sets as its denotation. Module
NTRIV gets a RWL loose theory, which has as denotations categories with an
interpretation of j as an associative binary functor, and which satisfies the couple
of choice transitions of NTRIV. The module import TRIV ! NTRIV corresponds to
an injective extra theory morphism T across the forgetful institution
MSA.
More formally, the inclusion signature morphism underlying T TRIV ! T NTRIV can
be represented as hu; ji where u is the institution morphism RWL ! MSA and j
is the signature inclusion S TRIV ! u(S NTRIV ) (where S TRIV is the MSA signature
of TRIV, S NTRIV is the RWL signature of NTRIV, and u(S NTRIV ) is the reduct of
S NTRIV to a MSA signature). Notice that u is an inclusion since the CafeOBJ cube
admits a trivial inclusion system in which all arrows are inclusions, that the reduct
from RWL signatures to MSA signatures is an identity, and that S TRIV ! S NTRIV is
an inclusion of MSA signatures.
An interesting aspect of this example is given by its model theory. The denotation
of this module import is the model reduct functor MOD(T NTRIV
in the CafeOBJ institution. From Definition 27, this means b u
which means a two level reduction. The first level, b u
, means getting rid of
the arrows of the carrier (i.e. making the carrier discrete) of the model and regarding
the interpretation of j as a function rather than functor. The second level,
MOD MSA (j), is a reduction internal to MSA which forgets the interpretation of
j . It is very important to notice that the correct denotation for this module import
can be achieved only in the framework of the CafeOBJ institution, the fact
that this is a Grothendieck institution being crucial. None of the institutions of the
CafeOBJ cube (such as RWL for example) would have been appropriate to give
the denotation of this example.
We denote the partial order of module imports by . By following the OBJ tradi-
tion, we can distinguish between three basic kinds of imports, protecting, extend-
ing, and using. At the level of the language, these should be treated just as semantic
declarations which determine the denotation of the importing module from the denotation
of the imported module.
Definition 37 Given a theory morphism model M of T , an expansion
of M along j is a model M 0 of T 0 satisfying the following properties:
the expansion is protecting,
there is an injective 16 model homomorphism M ,! M 0  j iff the expansion is
extending,
there is an arbitrary model homomorphism M!M 0  j iff the expansion is using,
and
with respect to j iff the expansion is free.
Definition 38 Fix an import SPSP 0 and let T and T 0 be the theories corresponding
to SP and SP 0 , respectively. Then
is an expansion of the same kind as the importation
mode involved of some model M 2 (and in addition free if SP 0 is initial) g.
Multiple imports are handled by a lattice structure on imports. The (finite) least
upper bounds (called sums in [15]) of module imports corresponds to the weak inclusion
system of theory morphisms being a proper inclusion system. In [16] we
lift sums from inclusion systems for ordinary theory morphisms to extra theory
morphisms; this result can be easily translated to the conceptual framework of Grothendieck
institutions. The (finite) greatest lower bounds (called intersections) are
defined as the pullback of the sums.
The details of this construction for the inclusion system of extra theory morphisms
are given in [16]; also this construction can be easily translated to the conceptual
framework of Grothendieck institutions.
In practice, one of the important properties of the sum-intersection square is to
be a pushout besides being a pullback square. This result for the inclusion system
of extra theory morphisms is given in [16]; again this can be easily translated to
Grothendieck institutions.
Under a suitable concept of 'injectivity'.
17 Which means that M 0 is the free object over M with respect to the model reduct functor
This relies the construction of finite limits in Grothendieck (fibred) categories.
4.2 Parameterisation
Parameterised specification and programming is an important feature of all module
systems of modern specification or programming languages. In CafeOBJ The
mathematical concept of parameterised modules is based on injections (in the sense
of Definition 34) in the category of theories of the CafeOBJ institution:
Parameterised specifications SP(X :: P) are modelled as injective theory
morphisms from the theory corresponding to the parameter P to the
theory corresponding to the body SP. Views are modelled as theory morphisms

The denotation [[SP]] of the body is determined from the denotation of the parameter
accordingly to the parameterisation mode involved as in the case of module imports
(Definition 38).
We distinguish two opposite approaches on parameters: a shared and a non-shared
one. In the 'non-shared' approach, the multiple parameters are mutually disjoint
(i.e.,
for X and X 0 two different parameters) and they are also
disjoint from any module imports T 0  T (i.e.,
0). In the 'shared'
approach this principle is relaxed to being disjoint outside common imports, i.e.,
two different parameters and
. The 'non-shared' approach has the potentiality
of a much more powerful module system, while the 'shared' approach seems
to be more convenient to implement (see [12] for details). The CafeOBJ definition
gives the possibility of the whole range of situations between these two extremes
by giving the user the possibility to control the sharing.
Example 39 This is an example adapted from [12]. Consider the (double param-
eterised) specification of a 'power' operation on monoids, where powers are elements
of another (abstract) monoid rather than natural numbers.
mod* MON {
mod* MON-POW (POWER :: MON, M :: MON)
{
vars
vars
The diagram defining MON-POW is
MON-POW
POWER
r
r
r
r
r
r
r
r
r
r
r
r
where MON-POW consists of two copies of MON (labelled by M and, POWER) re-
spectively, plus the power operation together with the 3 axioms defining its action.
This means TRIV is not shared, since the power monoid and the base monoid are
allowed to have different carriers. The denotation consists of all protecting
expansions (with interpretations of " ) to MON-POW of non-shared amalgamations
of monoids corresponding to the two parameters.
In the 'shared' approach, the parameterisation diagram is
MON
z
z
z
z
z
z
z
z
z
z
z
z
z
z
z
z
MON
POWER
In this case, the denotation consists of all two different monoid structures
on the same set, plus an interpretation of " satisfying the 'power' equations.
In CafeOBJ such sharing can be achieved by the user by the command share
which has the effect of enforcing that the modules declared as shared are included
rather than 'injected' in the body specification. In this case we have just to specify
share(TRIV)
The following defines parameter instantiation by pushout technique for the case of
single parameters. This definition can be naturally extended to the case of multiple
parameters (for details about instantiation of multiple parameters in CafeOBJ see
[12]).
be a parameterised module and let T its
representation as theory morphism. Let be a view. Then the instantiation
T SP (v) is given by the following pushout of theory morphisms in the CafeOBJ
institution:
in the 'non-shared' approach, and by the following co-limit
in the 'shared' approach.
The semantics of parameter instantiation relies on preservation properties of conservative
extensions by pushouts of theory morphisms. Recall the concept of conservative
theory morphism from [15]:
Definition 41 A theory morphism conservative iff any model M of T
has a protecting expansion along j.
Preservation of conservative extensions in Grothendieck institutions is a significantly
harder problem than in ordinary institutions. Such technical results for Grothendieck
institutions have been obtained in [16] but within the conceptual frame-work
of extra theory morphisms.
5 Conclusions and Future Work
We surveyed the logical foundations of CafeOBJ which constitute the origin of the
concrete definition of the language [12]. Some of its main features are:
simplicity and effectiveness via appropriate abstractness,
cohesiveness,
flexibility,
provides support for multi-paradigm integration,
provides support for the development of specification methodologies, and
uses state-of-art methods in algebraic specification research.
We defined the CafeOBJ institution, overviewed its main properties, and presented
the main mathematical concepts and result underlying basic and structured specification
in CafeOBJ.
Besides theoretical developments, future work on CafeOBJ will mainly concentrate
on specification and verification methodologies, especially the object-oriented
ones emerging from the behavioural specification paradigm. This includes refining
the existing object composition methodology based on projection operations
[30, 14, 12] but also the development of new methodologies and careful identification
of the application domains most suitable to certain specification and verification
methodologies.
The development of CafeOBJ has been an interplay process among language de-
sign, language and system implementation, and methodology development. Although
the language design is based on solid and firm mathematical foundations, it
has been greatly helped by the existence of a running system, which gave the possibility
to run various relevant examples, thus giving important feedback at the level
of concrete language constructs and execution commands. The parallel development
of methodologies gave special insight on the relationship between the various
paradigms co-existing in CafeOBJ with consequences at the level of design of the
language constructs.
We think that the interplay among mathematical semantic design of CafeOBJ, the
system implementation, and the methodology development has been the most important
feature of CafeOBJ design process. We believe this promises the sound
and reasonable development of a practical formal specification method around
CafeOBJ.



--R

The semantics of Clear
Principles of Maude.
Virgil Emil C













Principles of OBJ2.
Theorem Proving and Algebra.
Institutions: Abstract model theory for specification and programming.


A hidden agenda.



An initial algebra approach to the specification


Observational logic.

Categories for the Working Mathematician.




Some fundamental algebraic tools for the semantics of computation
--TR
Initiality, induction, and computability
Unifying functional, object-oriented and relational programming with logical semantics
Some fundamental algebraic tools for the semantics of computation, part 3
Conditional rewriting logic as a unified model of concurrency
Order-sorted algebra I
Institutions: abstract model theory for specification and programming
Logical support for modularisation
Principles of OBJ2
Membership algebra as a logical framework for equational specification
Towards an Algebraic Semantics for the Object Paradigm
Observational Logic
The Semantics of CLEAR, A Specification Language
Component-Based Algebraic Specification and Verification in CafeOBJ

--CTR
Rzvan Diaconescu, Herbrand theorems in arbitrary institutions, Information Processing Letters, v.90 n.1, p.29-37, 15 April 2004
Rzvan Diaconescu, Behavioural specification for hierarchical object composition, Theoretical Computer Science, v.343 n.3, p.305-331, 17 October 2005
Miguel Palomino, A comparison between two logical formalisms for rewriting, Theory and Practice of Logic Programming, v.7 n.1-2, p.183-213, January 2007
Mauricio Ayala-Rincn , Ricardo P. Jacobi , Luis G. A. Carvalho , Carlos H. Llanos , Reiner W. Hartenstein, Modeling and prototyping dynamically reconfigurable systems for efficient computation of dynamic programming methods by rewriting-logic, Proceedings of the 17th symposium on Integrated circuits and system design, September 07-11, 2004, Pernambuco, Brazil
Rzvan Diaconescu, Institution-independent Ultraproducts, Fundamenta Informaticae, v.55 n.3-4, p.321-348, August
Razvan Diaconescu, Institution-independent ultraproducts, Fundamenta Informaticae, v.55 n.3-4, p.321-348, June
Rzvan Diaconescu, Interpolation in Grothendieck institutions, Theoretical Computer Science, v.311 n.1-3, p.439-461, 23 January 2004
M. Ayala-Rincn , C. H. Llanos , R. P. Jacobi , R. W. Hartenstein, Prototyping time- and space-efficient computations of algebraic operations over dynamically reconfigurable systems modeled by rewriting-logic, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.11 n.2, p.251-281, April 2006
Francisco Durn , Jos Meseguer, Maude's module algebra, Science of Computer Programming, v.66 n.2, p.125-153, April, 2007
Narciso Mart-Oliet , Jos Meseguer, Rewriting logic: roadmap and bibliography, Theoretical Computer Science, v.285 n.2, p.121-154, 28 August 2002
behavioural specification;institutions;CafeOBJ;algebraic specification