Go backward to Example
Go up to Top
Go forward to Another Example

Other Properties

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.

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