# Computer Dictionary Online

Medical Dictionary   Law Dictionary   Legal Dictionary   Website Design
 0  1  2  3  4  5  6  7  8  9  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

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)

 Contact the Computer Dictionary Online  ::  Link to the Computer Dictionary Online  ::  Disclaimer for Computer Dictionary Online Computer Dictionary Online Copyright © 2018