More formally, a symbolic value expression is either *
Unknown* or an arbitrary arithmetic/conditional expression in terms of
constants,
variables, and loop indices. A * symbolic map*

binds variables to
symbolic descriptions of their values .
A symbolic map associated with a
region **R** may be either * relative* or * absolute*. In a *
relative* map, variables within bound values refer to their values on
entry to **R**; in an * absolute* map, no bound value may contain a
variable modified within **R**.

For convenience below, we define an operation on
symbolic map and symbolic value , which yields
* Unknown* if contains a not bound in ,
and otherwise yields with every occurrence of a
bound by replaced by the bound value .

Mon Oct 2 11:00:22 PDT 1995