Concretization and Abstract Post for Sign Analysis
Concrete domain : sets of states: (three variables)
Abstract domain :
Mapping: defined by:
Constructing an Abstract Lattice
Is a partial order? Yes, because of the properties of .
Is it a lattice?
For a fixed command,
The computed set of program states will contain the most precise set of program states.
Example: Take programs with two variables. Abstract states are pairs of signs. Take statement
x = x + y
and compute its abstract strongest postcondition sp#.