You are here: irt.org | FOLDOC | 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 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).
(1995-02-03)
Nearby terms: POWER « PowerBuilder « power cycle « powerdomain » PowerFuL » power hit » Power Mac
FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL