powerdomain

powerdomain
Hoare 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)