Lecturer
Norbert Preining
JAIST, Research Center for Software Verification, Japan
Place/Time
Mathematical Software and Free Documents XXI
2015-09-12, Kyoto, Japan.
Abstract
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.