-- ========================================================================
--         7 verification conditions for generate & check method
-- ========================================================================

-- ========================================================================
require genCases
require exState
require predCj

-- ========================================================================
-- theory module for formal parameter of module INV-1v etc.
mod* STEpcj {[Ste] [Pnm < PnmSeq] pred cj : PnmSeq Ste .}
-- ========================================================================
mod! INV-1v (ST :: STEpcj) {
ex(GENcases)
-- possible inductive invariant and target predicate
ops p-iinv p^t : -> PnmSeq . 
-- v_ is defined in the module GENcases
-- and is the predicate to be checked
[Ste < Val]
eq v(S:Ste) = cj(p-iinv,S:Ste) implies cj(p^t,S) .
}
-- ========================================================================
mod! INV-2v (ST :: STEpcj) {
ex(GENcases)
ops p-init p-iinv : -> PnmSeq .
-- v_ is defined in the module GENcases
-- and is the predicate to be checked
[Ste < Val]
eq v(S:Ste) = cj(p-init,S) implies cj(p-iinv,S) .
}

-- ========================================================================
-- theory module for formal parameter of module VALIDq etc.
mod* STE {[Ste]} 
-- ========================================================================
-- parameterized module for defining valid-q in [Lemma 7] and [Lemma 8]
mod! VALIDq (X :: STE) {inc(RWL)
-- predicate to be checked for all the transitions
pred q : Ste Ste .
** 'q' is supposed to be reified after 
** the parameter '(X :: STE)' is instantiated 
-- information constructor
[Infom] op (ifm _ _ _ _) : Ste Ste Bool Bool -> Infom {constr}
-- for checking conditions of ctrans rules
pred _then _ : Bool Bool .
eq (true  then B:Bool) = B . eq (false then B:Bool) = true .
-- predicate to be checked for a Ste
pred valid-q : Ste Ste Bool .
eq valid-q(S:Ste,SS:Ste,CC:Bool) =
     not(S =(*,1)=>+ SS if CC suchThat 
         not((CC then q(S, SS)) == true) {(ifm S SS CC q(S,SS))}) .
}
-- ========================================================================
-- parameterized module for Generate&Check-T1 and Generate&Check-T2
-- for reifying v_
mod! G&C-Tv (S :: STE) {
ex(VALIDq(S) + GENcases)
[Ste Bool < Val]
-- v_ is introduced in GENcases for being checked against all patterns
eq v(S:Ste,SS:Ste,CC:Bool) = valid-q(S,SS,CC) .
}

-- ========================================================================
mod! INV-3q (ST :: STEpcj) {
ex(G&C-Tv(ST))
ops pre post : -> PnmSeq .
-- 'q' is introduced in the module in the module G&C-Tv/VALIDq
-- and is the predicate to be checked
eq q(S:Ste,SS:Ste) = (cj(pre,S) implies cj(post,SS)) .
}

-- ========================================================================
-- theory module with p,q,m,cj on states
mod* STPQpcj {ex(PNAT)
[Ste] ops p q : Ste -> Bool . op m : Ste -> Nat.PNAT .
[Pnm < PnmSeq] op cj : PnmSeq Ste -> Bool .
}

-- ========================================================================
mod! PQ-1q (SQ :: STPQpcj) {
ex(G&C-Tv(SQ))
op pq-1-inv : -> PnmSeq .
eq q(S:Ste,SS:Ste) =  
      (cj(pq-1-inv,S) and p(S) and not(q(S))) implies (p(SS) or q(SS)) .
}

-- ========================================================================
mod! PQ-2q (SQ :: STPQpcj) {
ex(G&C-Tv(SQ))
op pq-2-inv : -> PnmSeq .
eq q(S:Ste,SS:Ste) =  
      (cj(pq-2-inv,S) and p(S) and not(q(S))) implies (m(S) > m(SS)) .
}

-- ========================================================================
mod! PQ-3v (SQ :: STPQpcj) {inc(RWL)
ex(GENcases)
op pq-3-inv : -> PnmSeq .
-- v_ is defined in the module GENcases
-- and is the predicate to be checked
[Ste < Val]
eq v(S:Ste,SS:Ste) =  
     (cj(pq-3-inv,S) and p(S) and not(q(S))) implies (S =(*,1)=>+ SS) .
}

-- ========================================================================
mod! PQ-4v (SQ :: STPQpcj) {
pr(GENcases)
op pq-4-inv : -> PnmSeq .
-- v_ is defined in the module GENcases
-- and is the predicate to be checked
[Ste < Val]
eq v(S:Ste) =  
   (cj(pq-4-inv,S) and (p(S) or q(S)) and (m(S) = 0)) implies q(S) .
}

-- ========================================================================
provide genCheck

-- ========================================================================
eof