分野別セミナー

Specification is description of model, and its verification is to show that the model has some desired properties by deducing the properties from the specification. As the proverb says “All models are wrong, some are useful”, and specification verification is an effective method for getting the useful models.


CafeOBJ is an executable algebraic specification language system which can be used as a specification verification system. CafeOBJ's specification is a set of conditional equations, and the deduction is equational inference. The equational inference can be executed by interpreting the specification's equations as left to right rewriting/reduction rules. This transparent view of CafeOBJ's specification verification makes the verification transparent. CafeOBJ language also has a powerful construct for parameterized modules, and it makes it easy to write well formed reusable specifications and proof scores (proof scripts).


This talk gives an overview of CafeOBJ, forcusing on recent developments in specification verification with proof scores.