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