The symbolic behavior of a region **R** is a relative map
describing every variable's value on exit in terms of enclosing
loop indices and variable values on entry to **R**. The following
operations are defined:

- : forms a map showing
the effect of the block on every program variable: unmodified
variables are mapped to themselves, modified variables are mapped to
a symbolic value expression representing the value on exit in terms of
the values on entry. New variables are
introduced to represent the values of certain operations with unknown
results (e.g., load from memory, I/O read). These variables are
limited in scope to the nearest enclosing loop or procedure body.
- Composition ():
apply to every bound value in :
- Meet (), with identity element :
- Iteration: finds loop invariants and induction
variables and rephrases them in terms of the given index variable
**i**. Auxiliary maps (loop invariants) and (induction variables) are used to compute , as follows:gives the net change after

**i**iterations of the loop, and includes loop invariant and induction variable recognition. - Closure: substitutes an expression
*if then else*for the most recent loop index variable**0****i**throughout . - : maps formals to actuals everywhere in .

Mon Oct 2 11:00:22 PDT 1995