Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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.
  
  
 
sav08/semantics_of_sign_analysis_domain.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice