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 add102 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>0We 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