Go backward to
Application of Execution Model
Go up to
Top
Go forward to
Unless
Fundamental Concepts
Three fundamental logical relations
Safety:
p
unless
q
.
Special case:
stable
p
.
Special case:
invariant
p
.
Progress:
p
ensures
q
Progress:
p
|->
q
(
p
leads-to
q
)
Safety and progress properties.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine