Partial Orders for Approximation

To solve complex constraints in numerical analysis, and in program analysis, we can use approximation techniques.

We use partial orders to describe approximation.

In numerical analysis the order is order on real numbers.

Example: if we are approximating some exact real value such as $\sqrt 2$ from above, then

$\begin{equation*} \sqrt 2 < 1.5 < 1.9 \end{equation*}$

and we have that $1.5$ is than $1.9$ in approximating $\sqrt 2$ .

In program analysis states often have discrete structures, so our orders are more like subset relations.

Example: if the set of possible values of a variable at some program point is $\{ 20, 21, 22 \}$ then we have

$\begin{equation*} \{ 20, 21, 22 \} \subseteq \{x.\ x \ge 20 \} \subseteq \{ x.\ x \ge 1 \} \subseteq \{ x.\ \mbox{true} \} \end{equation*}$

so among the three sets, $\{x.\ x \ge 20 \}$ is the best approximation of $\{ 20, 21, 22 \}$ .

To avoid working with all possible sets of states, we work with some subset of the set of states. This subset will form a structure such as lattice.

Basic plan:

represent semantics as limits of sequences in partial order elements (the Collecting Semantics)
approximate the semantics of a lattice with a simpler abstract lattice (used to represent space of loop invariants)
compute limits of sequences in the simpler abstract lattice
prove that approximation is conservative, a computed invariant is a always a true property (in worst case it is 'true')