Go backward to Rules of Superposition
Go up to Top
Go forward to Examples
The Superposition Theorem
Every property of the underlying program is a property of the
- If holds for of underlying program,
|| also holds because name no variables assigned in
. 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.
Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine