--
-- Invariants to Prove
--
-- Properties we discuss are invariants. 
-- In not only this example but also all examples used in this
-- seminar, only invariants are dealt with.
--
-- Invariants of a system are (safety) properties that are always true
-- in any reachable state of the system.
--
-- We prove two invariants on the system. 
-- One is what we want to prove, and the other is needed as a lemma 
-- to prove the former.
--

--
-- Claim 100 (**PROVED**) (Used Lemmas: 110)
--
--  invariants (x(s) >= 0)
--

--
-- Claim 110 (**PROVED**) (Used Lemmas: 100)
--
--  invariants (flag(s) implies x(s) >= 1)
--

--
-- Invariants to prove are defined as CafeOBJ terms in module INV.
--
mod INV {
  pr(INCDEC)
-- declare invariants to prove
  op inv100 : System -> Bool
  op inv110 : System -> Bool
-- CafeOBJ variables
  var S : System
-- define invariants to prove
  eq inv100(S) = (x(S) >= 0) .
  eq inv110(S) = (flag(S) implies x(S) >= 1) .
}

--
-- Invariants are proved by INDUCTION on the numbers of transition 
-- rules applied or executed. 
--
-- If we prove that the system has invariant P by induction on the
-- number of transition rules applied, 
-- the proof structure looks like this: 
--
--   I) Base case
--     P(init)
--   II) Inductive cases
--     1. P(s) implies P(inc(s)) for any s.
--     2. P(s) implies P(dec(s)) for any s.
--
-- The proof scores templates corresponding to this proof structure 
-- is found in template.mod.
--
-- Predicates to prove in each inductive step are defined as CafeOBJ
-- terms in module ISTEP.
--
mod ISTEP {
  pr(INV)
-- arbitrary objects
  -- s denotes an arbitrary state of the system.
  -- s' denotes the successor state after executing a transition rule in
  -- the state denoted by s.
  ops s s' : -> System
-- declare predicates to prove in inductive step
  op istep100 : -> Bool
  op istep110 : -> Bool
-- define predicates to prove in inductive step
  eq istep100 = inv100(s) implies inv100(s') .
  eq istep110 = inv110(s) implies inv110(s') .
}