Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:semantics_of_sign_analysis_domain [2009/03/26 13:23] 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. | ||