The purpose of this paper is to discuss the relationship between the interpretations of non-deterministic programs using the upper total correctness powerdomain on the one hand and the lower (partial correctness) powerdomain on the other. It is shown that there is a close semantic relationship between these two interpretations which suggests the formulation of a new operator called the mixed powerdomain. It is shown that the mixed powerdomain has many pleasing domain-theoretic and algebraic properties. The mixed powerdomain is closely related to new powerdomains which have been recently investigated as mathematical models of partial information in databases. Some of the basic intuitions captured by such structures may have uses for the specification of non-deterministic computations. The paper includes a sample non-deterministic programming language and a semantics using the mixed powerdomain.
|Original language||English (US)|
|Number of pages||14|
|Journal||Conference Record of the Annual ACM Symposium on Principles of Programming Languages|
|State||Published - 1990|
|Event||Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages - San Francisco, CA, USA|
Duration: Jan 17 1990 → Jan 19 1990
ASJC Scopus subject areas