Relating total and partial correctness interpretations of non-deterministic programs

Research output: Contribution to journalConference articlepeer-review

Abstract

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 languageEnglish (US)
Pages (from-to)306-319
Number of pages14
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
DOIs
StatePublished - 1990
Externally publishedYes
EventConference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages - San Francisco, CA, USA
Duration: Jan 17 1990Jan 19 1990

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Relating total and partial correctness interpretations of non-deterministic programs'. Together they form a unique fingerprint.

Cite this