LARA

Concretization and Abstract Post for Sign Analysis

Remember Sign Analysis for Expressions and Programs

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?

Abstract Postcondition

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#.