STeP verification conditions, easy-to-medium example, from the verification of mutual exclusion for a simple version of the Bakery algorithm: ------------------------------------------------------------------- invariant: pi0 = 0 \/ pi0 = 1 \/ pi0 = 2 \/ pi0 = 3 \/ pi0 = 4 invariant: pi1 = 0 \/ pi1 = 1 \/ pi1 = 2 \/ pi1 = 3 \/ pi1 = 4 invariant: pi0 <= 1 --> y1 = 0 invariant: pi1 <= 1 --> y2 = 0 invariant: 0 <= y2 invariant: 0 <= y1 invariant: (pi0=1 \/ pi0=4 \/ pi1=1 \/ pi1=4 \/ pi0=0 /\ y1 = 0 \/ pi1=0 /\ y2 = 0 \/ pi0=2 /\ y1 = y2 + 1 \/ pi0=3 /\ (y1 <= y2 \/ y2 = 0) \/ pi1=2 /\ y2 = y1 + 1 \/ pi1=3 /\ (y2 < y1 \/ y1 = 0)) Lemma : pi1=2 \/ pi1=3 \/ pi1=4 ==> 0 < y2 Lemma : pi0=2 \/ pi0=3 \/ pi0=4 ==> 0 < y1 ------------------------------------------------------------------ Assuming all of the above, prove each of the two goals below: ------------------------------------------------------------------ Goal 1 : ~(pi0 = 3 /\ pi1 = 2 /\ (y2 < y1 \/ y1 = 0)) Goal 2 : ~(pi0 = 2 /\ pi1 = 3 /\ (y1 <= y2 \/ y2 = 0)) ------------------------------------------------------------------