## powerdomain

<*theory*>

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

Last updated: 1995-02-03

### Nearby terms:

PowerBuilder ♦ power cycle ♦ **powerdomain** ♦ PowerFuL ♦ power hit ♦ Power Mac

Try this search on Wikipedia, OneLook, Google