• English only

Differences

This shows you the differences between two versions of the page.

sav08:semantics_of_sign_analysis_domain [2009/03/26 13:22]
vkuncak
sav08:semantics_of_sign_analysis_domain [2015/04/21 17:30] (current)
Line 1: Line 1:
====== Semantics of Sign Analysis Domain ====== ====== Semantics of Sign Analysis Domain ======
-
-Recall [[sav08:​Sign Analysis for Expressions and Programs]]

Concrete domain $C$: sets of states: $2^{\mathbb{Z}^3}$ (three variables) Concrete domain $C$: sets of states: $2^{\mathbb{Z}^3}$ (three variables)
Line 9: Line 7:
Mapping: $\gamma : A \to C$ defined by:  Mapping: $\gamma : A \to C$ defined by:
++++| ++++|
-$+\begin{equation*} \begin{array}{l} \begin{array}{l} \gamma(s_1,​s_2,​s_3) = \beta(s_1) \times \beta(s_2) \times \beta(s_3) \\ \gamma(s_1,​s_2,​s_3) = \beta(s_1) \times \beta(s_2) \times \beta(s_3) \\ Line 17: Line 15: \beta(\top) = \{ \ldots, -3,​-2,​-1,​0,​1,​2,​3,​\ldots \} \beta(\top) = \{ \ldots, -3,​-2,​-1,​0,​1,​2,​3,​\ldots \} \end{array} \end{array} -$+\end{equation*}
++++ ++++

Line 26: Line 24:

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

Is $\preceq$ a partial order? Is $\preceq$ a partial order?
Line 42: Line 40:

soundness condition: soundness condition:
-$+\begin{equation*} sp(\gamma(a)) \subseteq \gamma(sp\#​(a)) sp(\gamma(a)) \subseteq \gamma(sp\#​(a)) -$+\end{equation*}
The computed set of program states will contain the most precise set of program states. The computed set of program states will contain the most precise set of program states.