Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:semantics_of_sign_analysis_domain [2009/03/26 12:59] vkuncak |
sav08:semantics_of_sign_analysis_domain [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 7: | 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 15: | 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 24: | 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 40: | 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. | ||