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] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== 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) | ||
| - | |||
| - | Abstract domain $A$: $S^3$ | ||
| - | |||
| - | Mapping: $\gamma : A \to C$ defined by: | ||
| - | ++++| | ||
| - | \[ | ||
| - | \begin{array}{l} | ||
| - | \gamma(s_1,s_2,s_3) = \beta(s_1) \times \beta(s_2) \times \beta(s_3) \\ | ||
| - | \beta(neg) = \{-1,-2,-3,\ldots \} \\ | ||
| - | \beta(nul) = \{ 0 \} \\ | ||
| - | \beta(pos) = \{1,2,3,\ldots\} \\ | ||
| - | \beta(\top) = \{ \ldots, -3,-2,-1,0,1,2,3,\ldots \} | ||
| - | \end{array} | ||
| - | \] | ||
| - | ++++ | ||
| - | |||
| - | |||
| - | |||
| - | |||
| - | ===== Constructing an Abstract Lattice ===== | ||
| - | |||
| - | Define: | ||
| - | \[ | ||
| - | a_1 \preceq a_2 \iff \gamma(a_1) \subseteq \gamma(a_2) | ||
| - | \] | ||
| - | |||
| - | Is $\preceq$ a partial order? | ||
| - | Yes, because of the properties of $\subseteq$. | ||
| - | |||
| - | Is it a lattice? | ||
| - | |||
| - | ===== Abstract Postcondition ===== | ||
| - | |||
| - | For a fixed command, | ||
| - | |||
| - | $sp\# : A \to A$ | ||
| - | |||
| - | soundness condition: | ||
| - | \[ | ||
| - | sp(\gamma(a)) \subseteq \gamma(sp\#(a)) | ||
| - | \] | ||
| - | The computed set of program states will contain the most precise set of program states. | ||
| - | |||