Go backward to ExampleGo up to TopGo forward to Another Example |

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

- A behavior begins with
- 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

Author: Wolfgang Schreiner

Last Modification: May 14, 1998