CafeOBJ User's Manual 
-- ver.1.4.2 --

A.T. Nakagawa - Toshimi Sawada - Kokichi Futatsugi

July 17, 1999

 

Documentation revised and updated for CafeOBJ 1.4.2. A PostScript version is available; also at Jaist.

Warning: The contents of this document are likely to change.
It is advisable not to use links to any pages other than the first page (this page).

Changes from Version 1.3

The main changes from version 1.3 are as follows.

• In addition to Gnu Common Lisp, CMU Common Lisp and Allegro Common Lisp can be used as a platform.
• Faster rewrite engines are now available, and can be invoked from CafeOBJ.
• The predicate ==> (for transition relations) gets a more powerful support. A couple of new switches are added for this reason.
• Behavioural axioms can be used in equational reduction, and an operator attribute coherent is added for this purpose.
• A behavioural reduction command is introduced.
• Sort predicates are introduced.

Bibliography

1

Dershowitz, N. and Jouannaud, J.-P., ``Rewrite Systems'', Handbook of Theoretical Computer Science, Vol.B: Formal Models and Semantics, The MIT Press/Elsevier Science Publishers, 1990, pp.245-320

2

Diaconescu, R. and Futatsugi, K., Logical Semantics of CafeOBJ, Technical Report IS-RR-96-0024S, Japan Advanced Institute for Science and Teleology, 1996

3

Diaconescu, R. and Futatsugi, K., CafeOBJ Report, World Scientific, 1998

4

Ehrig, H. and Mahr, B., Fundamentals of Algebraic Specifications 1: Equations and Initial Semantics, Springer-Verlag, 1985

5

Goguen, J. and Burstall, R., ``Institutions: Abstract Model Theory for Specification and Programming'', Journal of the Association for Computing Machinery, Vol.39, 1992, pp.95-146

6

Goguen, J. and Diaconescu, R., ``An Oxford Survey of Order Sorted Algebra'', Mathematical Structures in Computer Science, Vol.4, 1994, pp.363-392

7

Goguen, J. and Malcom, G., A Hidden Agenda, technical report, UCSD, 1998

8

Goguen, J.A. and Meseguer, J., Order-Sorted Algebra 1: Equational Deduction for Multiple Inheritance, Polymorphism, Overloading and Partial Operations, Technical Report SRI-CSL-89-10, SRI International, 1989

9

Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., and Jouannaud, J.-P., Introducing OBJ, Technichal Report SRI-CSL-92-03, SRI International, 1992

10

Jacobs, B. and Rutten, J., ``A Tutorial on (Co)Algebras and (Co)Induction'', EATCS Bulletin, No.62, EATCS, 1997, pp.222-259

11

Klop, J.W., ``Term Rewriting Systems: A Tutorial'', EATCS Bulletin, No.32, EATCS, 1987, pp.143-182

12

Meseguer, J., ``Conditional Rewriting Logic: Deduction, Models and Concurrency'', Proc. 2nd International CTRS Workshop, Lecture Notes in Computer Science 516, 1991, pp.64-91

13

Meseguer,J. and Goguen,J.A., ``Initiality, induction and computability'', Algebraic Methods in Semantics, Cambridge University Press, 1984, pp.459-541

About this document ...

CafeOBJ User's Manual
-- ver.1.4.2 --

 This document was generated using the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -no_math -html_version 3.2,math -local_icons -split 4 -link 5 -dir doc -contents cont.html -index idx.html -t CafeOBJ Users' Manual cafeobj.tex.

The translation was initiated by Toshimi Sawada on 1999-07-17

1999-07-17