Language Design Laboratory
Developed by Professor Kokicih Futatsugi and his team from Japan Advanced Institute of Science and Technology's (JAIST) Language Design Laboratory, CafeOBJ is an advanced formal specification language for writing formal (i.e. mathematical) specifications of models for a wide variety of software and systems, and verifying their properties.
CafeOBJ is rigorously based on a logical system; or more precisely, it is a logical language, in the sense that its programs are sets of sentences in some logical system, and its operational semantics are given by deduction in that logical system. CafeOBJ uses order sorted algebra, which also provides a rigorous basis for user definable sub-types, exception handling, multiple inheritance, overloading, multiple representations, coercions, and more. It also supports user definable mixfix syntax, user definable execution strategies, rewriting modulo standard equational theories (associative, commutative, etc.), and selective memoization. It provides parameterized programming, with parameterized modules, module instantiation, views, module expressions, etc., to support very flexible program structuring and reuse.
CafeOBJ implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores in CafeOBJ, and do 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.
CafeOBJ is provided free of charge under the terms of the GNU General Public License version 2. It can be built to run on Mac OS X, Windows, or Linux.
For more information about and to download CafeOBJ, see here.
|Copyright © 2023 Franz Inc., All Rights Reserved | Privacy Statement