LARA

This is an old revision of the document!


Semantics of Sign Analysis Domain

Recall 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: \[

  a_1 \preceq a_2 \iff \gamma(a_1) \subseteq \gamma(a_2)

\]

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: \[

  sp(\gamma(a)) \subseteq \gamma(sp\#(a))

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