Program name
initially initial values of superposed variables
transform effect of augmentation rule
add effect of restricted union rule
- Augmentation Rule:
- Statement in underlying program may be transformed to
|| where does not assign to underlying variables.
- Restricted Union Rule:
- Statement may be added to underlying program provided that does
not assign to underlying variables.