A Cook's Tour of Countable Nondeterminism

DAIMI Report Series

View Publication Info
Field Value
Title A Cook's Tour of Countable Nondeterminism
Creator Apt, K. R.
Plotkin, Gordon D.
Description We provide four semantics for a small programming language involving unbounded (but countable) nondeterminism. These comprise an operational one, two denotational ones based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. We also introduce a Hoare-like proof system for total correctness and show its soundness and completeness in an appropriate sense. Admission of countable nondeterminism results in a lack of continuity of various semantic functions; moreover some of the partial orders considered are in general not cpo's and in proofs of total correctness one has to resort to the use of (countable) ordinals. Proofs will appear in the full version of the paper.
Publisher Aarhus University
Date 1981-01-01
Type info:eu-repo/semantics/article
Peer-reviewed Article
Format application/pdf
Identifier http://ojs.statsbiblioteket.dk/index.php/daimipb/article/view/18448
Source DAIMI Report Series; No 133 (1981): PB-133 A Cook's Tour of Countable Nondeterminism
DAIMI Report Series; No 133 (1981): PB-133 A Cook's Tour of Countable Nondeterminism
Language eng
Relation http://ojs.statsbiblioteket.dk/index.php/daimipb/article/view/18448/16105

Contact Us

The PKP Index is an initiative of the Public Knowledge Project.

For PKP Publishing Services please use the PKP|PS contact form.

For support with PKP software we encourage users to consult our wiki for documentation and search our support forums.

For any other correspondence feel free to contact us using the PKP contact form.

Find Us


Copyright © 2015-2018 Simon Fraser University Library