Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Volume 19 / Issue 6

available in:   PDF (191 kB) PS (203 kB)
 
get:  
Similar Docs BibTeX   Write a comment
  
get:  
Links into Future
 
DOI:   10.3217/jucs-019-06-0771

 

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

Kazuhiro Ogata (Japan Advanced Institute of Science and Technology (JAIST), Japan)

Kokichi Futatsugi (Japan Advanced Institute of Science and Technology (JAIST), Japan)

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) p0) and p(υ) ∧ q(υ) ⇒ p(υ′), and (2) q0) 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) q0) 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) q0) 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: CafeOBJ, algebraic specification, invariant, observational transition system (OTS), simultaneous induction

Categories: D.2.4, F.3.1