This is an old revision of the document!
Semantics of Sign Analysis Domain
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
.
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.