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
.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998