This is an old revision of the document!
Semantics of Sign Analysis Domain
Constructing an Abstract Lattice
Definibe: \[
a_1 \preceq a_2 \iff \gamma(a_1) \subseteq \gamma(a_2)
\]
Is a partial order? Yes, because of the properties of .
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.