Concretization and Abstract Post for Sign Analysis

Concrete domain $C$ : sets of states: $2^{\mathbb{Z}^3}$ (three variables)

Abstract domain $A$ : $S^3$

Mapping: $\gamma : A \to C$ defined by:

Constructing an Abstract Lattice

Define:

$\begin{equation*} a_1 \preceq a_2 \iff \gamma(a_1) \subseteq \gamma(a_2) \end{equation*}$

Is $\preceq$ a partial order? Yes, because of the properties of $\subseteq$ .

Is it a lattice?

For a fixed command,

$sp\# : A \to A$

soundness condition:

$\begin{equation*} sp(\gamma(a)) \subseteq \gamma(sp\#(a)) \end{equation*}$

The computed set of program states will contain the most precise set of program states.

Example: Take programs with two variables. Abstract states are pairs of signs. Take statement

x = x + y

and compute its abstract strongest postcondition sp#.