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 role in structuring the language design. (C) 2002 Elsevier Science B.V. All rights reserved.
cafeobj algebraic specification institutions behavioural specification