Go up to Top
Go forward to Invariance Properties

Proving Simple Program Properties

Program P:
- var natural $x$ , $y$ = 0
  do
  <true -> $x$ := $x+1$ >
  []
  <true -> $y$ := $y+1$ >
  od
TLA Formula Phi:
- Init_Phi $<=>$ $(x=0)$ and $(y=0)$
- A₁ $<=>$ $(x' = x+1)$ and $(y' = y)$
- A₂ $<=>$ $(y' = y+1)$ and $(x' = x)$
- A $<=>$ A₁ or A₂
- Phi $<=>$ Init_Phi and always [A]_{<x, y>}
  and WF_{<x, y>}(A₁) and WF_{<x, y>}(A₂)
Program P has property F:
- Phi $=>$ $F$

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

Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine

Next