a *semantic function*. A semantic algebra consists of a *universe* which defines the space of possible program meanings, and *sequencing*, *choice*, and *iteration* operators, which define how to compose program meanings. A semantic function is a mapping from control flow edges to elements of the universe which defines the meaning of each control flow edge. A path expression is *evaluated* by interpreting the individual edges using the semantic function, and interpreting the regular expression operators using the corresponding operators of the semantic algebra (to compose the interpretations of individual edges into interpretations of sets of program paths).

Keeping this overall algorithm in mind, we proceed to describe the interpretation which defines linear recurrence analysis.

#### **LRA Universe.**

The semantic universe of LRA (i.e., the space of program meanings) is the set of (not necessarily linear) arithmetic *transition formulas*. If we let ${\textsf{Var}}$ denote the set of program variables and ${\textsf{Var}}'$ the set of “primed” copies of program variables, then a transition formula is an arithmetic formula with free variables in ${\textsf{Var}}\cup {\textsf{Var}}'$. Such a formula represents an input/output relation between program states.

#### **LRA Semantic Function.**

The semantic function ${\llbracket \cdot \rrbracket}$ is a function that maps each edge of 