Go backward to Another Program
Go up to Top
Go forward to Mapping the Program to Machines

Proof of Correctness

  1. Invariant holds at all execution points:
    • invariant 0 <=r
      and (for all u where 0 <= u < r :: not com(u))
    • Invariant is true initially.
    • Invariant is true after r := f(r).
  2. FP := (r = f(r) and r = g(r) and r = h(r)).
    • Fixed point reached when := becomes =.
    • FP implies com(r).
    • (1) and (2) prove that when P2 reaches fixed point, r is the minimum meeting time.
  3. P2 always reaches fixed point:
    • not FP and r = k implies r > k at some later point.
    • (1) shows that r cannot increase beyond z.
    • Eventually FP must hold.
UNITY provides a full proof theory.

Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: intro.tex,v 1.2 1996/01/31 15:37:03 schreine Exp schreine

Prev Up Next