Go backward to
Special Cases of Unless
Go up to
Top
Go forward to
Leads-to
Ensures
p
ensures
q
<=>
(
p
unless
q
and
<
exists
s
:
s
in
F
:: {
p
and
not
q
}
s
{
q
}>)
If
p
is true at some point in computation, then
p
remains true as long as
q
is false,
and eventually
q
becomes true.
Program execution model:
p
[
R
i
]
=>
<
exists
j
:
j
>=
i
::
q
[
R
j
]
and
<
forall
k
:
i
<=
j<k
::
p
[
R
k
]>>
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine