JUCS - Journal of Universal Computer Science 19(6): 771-804, doi: 10.3217/jucs-019-06-0771

Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method

‡ Japan Advanced Institute of Science and Technology (JAIST), Nomi, Japan§ Japan Advanced Institute of Science and Technology, Nomi, Japan

Corresponding author: Kazuhiro Ogata ( ogata@jaist.ac.jp ) © Kazuhiro Ogata, Kokichi Futatsugi. This article is freely available under the J.UCS Open Content License. Citation:
Ogata K, Futatsugi K (2013) Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method. JUCS - Journal of Universal Computer Science 19(6): 771-804. https://doi.org/10.3217/jucs-019-06-0771 |

Abstract

Observational transition systems (OTSs) are state machines that can be described as behavioral specifications in CafeOBJ, an algebraic specification language and processor. The OTS/CafeOBJ method uses OTSs and CafeOBJ for systems specification and verification. Simultaneous induction is intensively used to prove that an OTS enjoys invariants in the method. To prove that two state predicates p and q are invariants with respect to an OTS S, simultaneous induction generates the proof obligations: (1) p(υ0) and p(υ) ∧ q(υ) ⇒ p(υ′), and (2) q(υ0) and p(υ) ∧ q(υ) ⇒ q(υ′) for each initial state υ0, each state υ and each successor state υ′ of υ. Instead, we may also use the proof obligations: (1) q(υ) ⇒ p(υ), and (2) q(υ0) and p(υ) ∧ q(υ) ⇒ q(υ′). The proof technique generating proof obligations like this is called semi-simultaneous induction. The proof obligation is equivalent to (1) q(υ) ⇒ p(υ), and (2) q(υ0) and q(υ) ⇒ q(υ′). But, the former may need less cases, making proofs shorter, than the latter. More importantly, the former makes it possible to record the process in which way lemmas have been conjectured. This article demonstrates some benefits of (semi)simultaneous induction, describes semi-simultaneous induction and justifies it.

Keywords

algebraic specification, CafeOBJ, invariant, observational transition system (OTS), simultaneous induction