CafeOBJ 1.5.5 released

Yesterday we have released CafeOBJ 1.5.5 with a long list of changes, and many more internal changes. Documentation pages have been updated with the latest reference manual (PDF, Html) as well as some new docs on CITP (in Japanese for now) and tutorials.

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

• Enhancemets of a family of Bool term inspector commands:
  • binspect [ in : <Modexpr> ] <bool-term> . converts given <bool-term> into abstracted xor-and normal form
  • bshow [ tree | grind ] shows abstracted Bool term
  • bresolve [ <num1> [ { <num2> | all } ] ] shows assignments which make abstracted Bool term true
  • bguess { imply | and | or } tries with some heuristics to solve the abstracted Bool term
• bug fix in ACZ rewriting
• CITP changes
  • :ctf [ <term> ] accepts constructors with arguments
  • new command :imply to make instantiated lhs of existing equation of the form eq lhs = true a premise of a goal sentence
  • new tactic rd- which is similar to rd but cancels the normalization of the goal sentence if the sentence is not satisfied
• new switch tree horizontal. if on show term tree displays the term tree structure horizontally (default off).

Availability

Binary packages for Windows, MacOS, and Linux have been built, and can be found at the CafeOBJ download page. The source code can also be found on the download page, or directly from here: cafeobj-1.5.5.tar.gz.

The CafeOBJ Debian package will be updated soon.

Macports file has also been updated, please see the above download/install page for details how to add our sources to your macport.

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