Repository | Series | Book | Chapter
Some tips on writing proof scores in the ots/cafeobj method
pp. 596-615
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.
Publication details
Published in:
Futatsugi Kokichi, Jouannaud Jean-Pierre, Meseguer José (2006) Algebra, meaning, and computation: essays dedicated to Joseph A. Goguen on the occasion of his 65th birthday. Dordrecht, Springer.
Pages: 596-615
DOI: 10.1007/11780274_31
Full citation:
Ogata Kazuhiro, Futatsugi Kokichi (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, 596–615.