powerdomain

theory 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:

Egli-Milner:

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 abstractinterpretation 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).

(1995-02-03)