The system consists of two processes called Inc and Dec. The processes share integer variable x. Process Inc repeatedly increments x, and process Dec decrements x if another boolean variable flag is true. Variable x is initially 0 and variable falg is initially false. Variable flag is set to true by process Inc if the process increments variable x and variable flag is set to false by process Dec if the process decrements variable x.
CafeOBJ specification of the system.
- invariants.mod Invariants to prove.
- template.mod Proof scores templates.
- proof100.mod Proof score of Claim 100.
- proof110.mod Proof score of Claim 110.