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

sav08/semantics_of_sign_analysis_domain.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice 