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 .