Repository | Book | Chapter
(2006) Algebra, meaning, and computation, Dordrecht, Springer.
Some tips on writing proof scores in the ots/cafeobj method
Kazuhiro Ogata, Kokichi Futatsugi
pp. 596-615
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.
Publication details
DOI: 10.1007/11780274_31
Full citation:
Ogata, K. , Futatsugi, K. (2006)., Some tips on writing proof scores in the ots/cafeobj method, in K. Futatsugi, J. Jouannaud & J. Meseguer (eds.), Algebra, meaning, and computation, Dordrecht, Springer, pp. 596-615.