- What about more complicated properties"
- A behavior begins with $x$ and $y$ both zero, and repeatedly increments either $x$ or $y$ (in a single operation), choosing non-deterministically between them, but choosing each infinitely many times.

- Exactly our formula
`Phi`!- No distinction between program and property.
- View
`Phi`as*description*of program. - View
`Phi`as*specification*of program.

- Consider a program
`Psi`.- Show that
`Psi`$=>$`Phi`.

- Show that

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

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