- 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)*.

`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.

`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.

Wolfgang.Schreiner@risc.uni-linz.ac.at

Id: intro.tex,v 1.2 1996/01/31 15:37:03 schreine Exp schreine