Logical Semantics for CafeOBJ (abstract)
This document presents the semantics of CafeOBJ system and
language. CafeOBJ can be seen as a succesor of the famous algebraic
specification and programming language OBJ but adding several new
paradigms to the traditional OBJ language, such as specification of
concurrent systems, object-orientation, and behavioural specification.
CafeOBJ is a declarative language in the same way other OBJ-family
languages (OBJ, Eqlog, FOOPS, Maude) are. Therefore the formal semantics of
CafeOBJ follows the same general principle:
There is an underlying logic (i.e., institution) in which all basic
constructs/features of the language can be rigorously explained.
This intimate relationship between the language and its underlying
logic was called ``logical programming'' by Goguen and Meseguer.
In providing the semantics for CafeOBJ we distinguish between four
levels of the language:
- programming ``in the small''
- programming ``in the large''
- programming ``in the huge''
- environment.
Programming ``in the small'' refers to collections of program
statements (as obtained by flattening the individual modules,
programming ``in the large'' to the module interconnection system,
programming ``in the huge'' to the software system composition, and
the environment to the set of tools (including methodologies)
supporting the process of programming and specification building in
CafeOBJ. While programming in the small and in the large require
formal mathematical semantics, programming in the huge can be
approached semantically using some general techniques developed for
programming in the large, the environment cannot (and should not) be
given formal semantics. However we devote a brief section to
the latter because this is an essential aspect of the
CafeOBJ system which should be understood in relationship to
the former levels. So we formulate the second principle of
our semantics:
Provide an integrated, cohesive, and unitary approach to the
semantics of programming/specification in the small and in the large.
The third principle refers to the methodology of developing the
logical semantics:
Develop all ingredients (concepts, results, etc.) at the highest
appropriate level of abstraction.
In order to achieve this we make extensive use of the powerful modern
semantic tools made available by research in algebraic specification
over the past decade, such as institutions and category
theory. Institutions make it perfect for developing the semantics of
sophisticated systems implementing a multitude of mutually
interacting paradigms in a simple, clean, and compact manner. Modern
systems, including CafeOBJ, cannot escape a certain degree of
complexity and sophistication, however institutions (and more
generally, categorical methods) greatly help in retaining a basic
simplicity at least at the level of semantics. Moreover, our abstract
logical approach permits future extensions of CafeOBJ with other
paradigms provided they are rigorously based on logic and they
interact well with the existing paradigms; such extensions will still
lie within the present semantics.
Finally, this document does not address the detalied mathematical
aspects of this semantics (which sometimes could be rather
sophisticated) but rather give pointers to other documents backing our
claims. However, we provide in the appendices very brief surveys of
several key structures; we hope this will make this document more self
contained.
full paper--50K.
Back to CafeOBJ Home Page