-------------------------------- MODULE ex2 --------------------------------
EXTENDS Naturals
CONSTANTS a,b
VARIABLES  x,y,pc
---------------------------------------------------------------------
(* Define actions from the text of annotated algorithm *)
al1l2 ==
    /\ pc="l1"
    /\ pc'="l2"
    /\ x'=y /\ y'=x
---------------------------------------------------------------------    
(*  Define  the computation relation *)
next == al1l2
(* Define the initial conditions *)
init == pc="l1" /\ x=a /\ y=b
---------------------------------------------------------------------    
(* Define the invariant from the annotation *)    
i == 
    /\ pc="l1" => x=a /\ y=b
    /\ pc="l2" => x=b /\ y=a
(* Define the safety property to check namely the partial correctness *)    

safe == pc="l2" => x=b /\ y=a


=============================================================================
\* Modification History
\* Last modified Wed Sep 09 17:29:46 CEST 2015 by mery
\* Created Wed Sep 09 17:24:19 CEST 2015 by mery