Proof Scores in the OTS/CafeOBJ Method

A way to write proof scores showing that distributed systems have invariant properties in algebraic specification languages is described, which has been devised through several case studies. The way makes it possible to divide a formula stating an invariant property under discussion into reasonably small ones, each of which is proved by writing proof scores individually. This relieves the load to reduce logical formulas and can decrease the number of subcases into which the case is split in case analysis.

• Type: Conference
• Year: 2003
• Where: FMOODS
• Authors: Kazuhiro Ogata, Kokichi Futatsugi
• Keywords: Algebraic Specification Languages, FMOODS 2003, FMOODS 2007, Invariant Properties, Proof Scores