powerdomain

powerdomain

(theory)The powerdomain of a domain D is a domaincontaining some of the subsets of D. Due to the asymmetrycondition in the definition of a partial order (andtherefore of a domain) the powerdomain cannot contain all thesubsets of D. This is because there may be different sets Xand Y such that X <= Y and Y <= X which, by the asymmetrycondition would have to be considered equal.

There are at least three possible orderings of the subsets ofa powerdomain:

Egli-Milner:

X <= Y iff for all x in X, exists y in Y: x <= yand for all y in Y, exists x in X: x <= y

("The other domain always contains a related element").

Hoare or Partial Correctness or Safety:

X <= Y iff for all x in X, exists y in Y: x <= y

("The bigger domain always contains a bigger element").

Smyth or Total Correctness or Liveness:

X <= Y iff for all y in Y, exists x in X: x <= y

("The smaller domain always contains a smaller element").

If a powerdomain represents the result of an abstract interpretation in which a bigger value is a safeapproximation to a smaller value then the Hoare powerdomain isappropriate because the safe approximation Y to thepowerdomain X contains a safe approximation to each point inX.

("<=" is written in LaTeX as \\sqsubseteq).