Go backward to
Ensures
Go up to
Top
Go forward to
Fixed Point
Leads-to
p
|->
q
Derived by a finite number of applications of the following inference rules:
p
ensures
q
p
|->
q
p
|->
q
q
|->
r
p
|->
r
<
forall
m
:
m
in
W
::
p
(
m
)
|->
q
>
<
exists
m
:
m
in
W
::
p
(
m
)>
|->
q
Once that
p
becomes true,
q
is or will be true.
Cannot assure that
p
will remain true as long as
q
is not.
Program execution model:
p
[
R
i
]
=>
<
exists
j
:
j
>=
i
::
q
[
R
j
]>
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine