A simple example: a double counter

add10 : SYSTEM 
 BEGIN 
 x , y : VAR nat
 BEGIN 

  x < 10                   ---> x ::= x + 1 []
  (x = 10 and y < 10)      ---> y ::= y + 1 []
  y >= 10                  ---> y ::= y - 1 []
  (y = 0 and x > 0)        ---> x ::= x - 1 []
      END 
    
  INITIALLY   :  x = 0 and  y = 0
 END add10

2 tivially valid TCCs due to the fact that x and y are positive numbers are generated for system add10 :

add10_Tcc_1 : y>=10 => y-1>0

add10_Tcc_2 :y=0 and x>0 => x-1>0

We want to prove that x<=10 and y<=10 is an invariant of the system add10. Four valid verification conditions are generated:

VC_1 : OBLIGATION (x<=10 and y<=10) and x < 10
                    implies (x+1<=10 and y<=10)

VC_2 : OBLIGATION (x<=10 and y<=10) and (x = 10 and y < 10)
                    implies (x<=10 and y+1<=10)

VC_3 : OBLIGATION (x<=10 and y<=10) and y >= 10
                    implies (x<=10 and y-1<=10)

VC_4 : OBLIGATION (x<=10 and y<=10) and (y = 0 and x > 0)
                    implies (x-1<=10 and y<=10)

Back to the Invariant Checker home page