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
 
Contributor
 
Date 1981-01-01
 
Type info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
Peer-reviewed Article
 
Format application/pdf
 
Identifier http://ojs.statsbiblioteket.dk/index.php/daimipb/article/view/18448
10.7146/dpb.v10i133.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
2245-9316
0105-8517
 
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

Twitter

Copyright © 2015-2018 Simon Fraser University Library