This is an old revision of the document!
Semantics of Sign Analysis Domain
Recall Sign Analysis for Expressions and Programs
Concrete domain : sets of states: (three variables)
Abstract domain :
Mapping: defined by:
Constructing an Abstract Lattice
Define: \[
a_1 \preceq a_2 \iff \gamma(a_1) \subseteq \gamma(a_2)
\]
Is a partial order? Yes, because of the properties of .
Is it a lattice?
Abstract Postcondition
For a fixed command,
soundness condition: \[
sp(\gamma(a)) \subseteq \gamma(sp\#(a))
\] The computed set of program states will contain the most precise set of program states.