Generic Proof Scores for Generate & Check Method in CafeOBJ.

Generic proof scores for the generate & check method in CafeOBJ are described. The generic proof scores codify the generate & check method as parameterized modules in the CafeOBJ language independently of specific systems to which the method applies. Basic proof scores for a specific system can be obtained by instantiating the formal parameter modules of the parameterized modules with the actual specification modules of the specific system. The effectiveness of the generic proof scores is demonstrated by applying them to a couple of non-trivial examples.