Overview

CafeOBJ is a most advanced formal specification language which inherits many advanced features (e.g. flexible mix-fix syntax, powerful and clear typing system with ordered sorts, parameteric modules and views for instantiating the parameters, and module expressions, etc.) from OBJ (or more exactly OBJ3) algebraic specification language.

CafeOBJ is a language for writing formal (i.e. mathematical) specifications of models for wide varieties of software and systems, and verifying properties of them. CafeOBJ implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and doing proofs by executing the proof scores.

CafeOBJ has state-of-art rigorous logical semantics based on institutions. The CafeOBJ cube shows the structure of the various logics underlying the combination of the various paradigms implemented by the language. Proof scores in CafeOBJ are also based on institution based rigorous semantics, and can be constructed using a complete set of proof rules.

News

  • CafeOBJ 1.6.0 released - We have released a new version of CafeOBJ, which incorporates the following changes: CITP is officially renamed to PTcalc documents are not updated yet PTcalc (CITP) enhancements :init defined by :def is evaluated in the proof node to which it is applied :init can be without substitution Search predicate enhancements nested search is properly handled […]
  • CafeOBJ 1.5.9 released - We have released a new version of CafeOBJ, which incorporates the following changes: improved memoization higher heap allocation on 64bit systems fixes to .cafeobj file handling new switch ‘show every finding’ optimization fixes and dead code removal Please see the download page for the source release, binary packages, and installation instructions. Please report bugs to […]
  • CafeOBJ 1.5.8 released - We have released a new version of CafeOBJ, which incorporates new commands and fixes for CITP. Please see the download page for the source release, binary packages, and installation instructions. For the moment Windows builds are only available based on Allegro CL due to incompatibilities between Windows SBCL and CafeOBJ. CafeOBJ 1.5.8 has already been […]
  • CafeOBJ 1.5.7 released - We have released a new version of CafeOBJ, which incorporates mostly fixes for CITP as well as updates to work with newer versions of SBCL. Please see the download page for the source release, binary packages, and installation instructions. For the moment Windows builds are only available based on Allegro CL due to incompatibilities between […]
  • Book published: Introduction to programming for model description and validation (in Japanese) - Prof. Futatsugi’s book Introduction to programming for model description and validation (モデルの記述と検証のためのプログラミング入門) has been published this week and will be available from various outlets and online. The web site of the book provides access to downloadable versions of the code given in the book.