Go backward to Program Composition by Union
Go up to Top
Go forward to Proof of Union Theorem
The Union Theorem
- unless in []
( unless in
and unless in )
- If is true and is not, remains true or
becomes true.
- ensures in []
[ ensures in
and unless in ] or
[ ensures in
and unless in ]
- If is true, remains true as long as is false and
eventually becomes true.
- (FP of [] )
(FP of ) and (FP of )
- State does not change any more.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine