• 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) Both sides previous revision Previous revision 2009/03/26 13:23 vkuncak 2009/03/26 13:22 vkuncak 2009/03/26 13:22 vkuncak 2009/03/26 12:59 vkuncak 2009/03/26 12:59 vkuncak 2009/03/25 11:05 vkuncak 2009/03/25 01:56 vkuncak 2008/05/07 23:29 giuliano 2008/05/07 23:26 giuliano 2008/05/07 08:21 vkuncak 2008/05/07 02:06 vkuncak 2008/05/07 02:02 vkuncak 2008/05/07 02:01 vkuncak 2008/05/07 02:01 vkuncak created Next revision Previous revision 2009/03/26 13:23 vkuncak 2009/03/26 13:22 vkuncak 2009/03/26 13:22 vkuncak 2009/03/26 12:59 vkuncak 2009/03/26 12:59 vkuncak 2009/03/25 11:05 vkuncak 2009/03/25 01:56 vkuncak 2008/05/07 23:29 giuliano 2008/05/07 23:26 giuliano 2008/05/07 08:21 vkuncak 2008/05/07 02:06 vkuncak 2008/05/07 02:02 vkuncak 2008/05/07 02:01 vkuncak 2008/05/07 02:01 vkuncak created 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.