Go backward to Example
Go up to Top
Go forward to Another Example
- What about more complicated properties"
- A behavior begins with and both zero, and repeatedly increments either
or (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.
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine