Every property of the underlying program is a property of the transformed program.

- Augmentation:
- If $\{p\}\; s\; \{q\}$ holds for $s$ of underlying program, $\{p\}\; s$ || $r\; \{q\}$ also holds because $p,q$ name no variables assigned in $r$. Since furthermore initial condition of underlying program is preserved, all proofs are preserved.

- Restricted Union:
- Added statements do not write into underlying variables. From locality corollary and the fact that underlying program does not mention superposed variables in its proof, all proofs are preserved.

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine $$