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