Some tips on writing proof scores in the ots/cafeobj method

Kazuhiro Ogata

Kokichi Futatsugi

pp. 596-615

in: Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer (eds), Algebra, meaning, and computation, Berlin, Springer, 2006

Abstract

The OTS/CafeOBJ method is an instance of the proof score approach to systems analysis, which has been mainly devoted by researchers in the OBJ community. We describe some tips on writing proof scores in the OTS/CafeOBJ method and use a mutual exclusion protocol to exemplify the tips. We also argue soundness of proof scores in the OTS/CafeOBJ method.