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

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


X <= Y iff for all x in X, exists y in Y: x <= y and 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 safe approximation to a smaller value then the Hoare powerdomain is appropriate because the safe approximation Y to the powerdomain X contains a safe approximation to each point in X.

("<=" is written in LaTeX as \sqsubseteq).
References in periodicals archive ?
The event diagram together with the set of pending messages is said to form a powerdomain which is used to describe the concurrency of Actors.
perpendicular to]]), where P is the Hoare powerdomain operator and [perpendicular to] denotes undefinedness (i.
1986, Section 4], the concrete domains are given by the Hoare powerdomains P([N.
It provides, for any suitable domain D, the powerdomain P(D) whose elements are subsets of D.
It contains a section on powerdomains, which were originally published in [32].
Another solution is presented by Ferguson and Hughes [1989] who consider a particular collection of convex sets: the cone powerdomain.
Powerdomains and nondeterministic recursive functions.
Powerdomains and predicate transformers: A topological view.