Yesterday we have finally released CafeOBJ 1.5.0. This marks a great step forward in a long development history of this algebraic specification and verification language.
To quote from our README:
CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.
Changes
Many changes have been done over the years, here I mention only a few recent additions:
- introduction of a large family of search predicates for state/transition based specifications (see `search predicates’ in the online help or manual)
- addition of a (nearly) complete reference manual (reference-manual.pdf)
- addition of CITP-like proving tool (see this site for the original version)
- revised build system, allows for building and running CafeOBJ based on several lisp engines
- improved online help system with search functionality (see `?’ `?ap’ etc)
- build support has been stream-lined, currently supported Common Lisp implementations are SBCL, CLISP, Allegro CL
Availability
Binary packages for Windows, MacOS, and Linux have been built, and can be found at the Bitbucket download page. The source code is also available from the bitbucket page, or from here: cafeobj-1.5.0.tar.gz.
Packages for inclusion into Debian have been submitted and are in NEW processing.
Other distributions might follow in the future.
Bug reports
If you find a bug, have suggestions, or complains, please open an issue at the issue tracker for CafeOBJ.
For other inquiries, please use info@cafeobj.org