Algebraic specifications and Functional programming with CafeOBJ


Norbert Preining
JAIST, Research Center for Software Verification, Japan


Mathematical Software and Free Documents XXI
2015-09-12, Kyoto, Japan.


CafeOBJ is an algebraic specification language based on equational order-sorted logic, which incorporates rewriting logic and hidden algebras. What sets it apart from other specification languages is that it is also executable, means that specifications can be `executed’ or rewritten to prove properties. Furthermore, its flexible mix-fix syntax, powerful module system including inheritance and parametrized modules, it has the potential to function efficiently in various circumstances, including symbolic and algebraic computations.

In this talk we give a short introduction to CafeOBJ, go through a few examples of functional programming with CafeOBJ, and present an example of an algebraic specification and verification of its properties.

Leave a comment

Your email address will not be published. Required fields are marked *