Go backward to
A Simple Program
Go up to
Top
Go forward to
Proof of Correctness
Another Program
Program
P2
initially
r
= 0
assign
r
:=
f(r)
[]
r
:=
g(r)
[]
r
:=
h(r)
end
{
P2
}
Non-deterministic selection of assignments.
Fairness: no assignment is indefinitely blocked.
Is program correct?
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: intro.tex,v 1.2 1996/01/31 15:37:03 schreine Exp schreine
