Countable nondeterminism and random assignment

Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalenc...

Full description

Saved in:
Bibliographic Details
Published in:Journal of the ACM 1986-10, Vol.33 (4), p.724-767
Main Authors: APT, K. R, PLOTKIN, G. D
Format: Article
Language:English
Subjects:
Applied sciences
Completeness
Computer science
control theory
systems
Continuity
Equivalence
Exact sciences and technology
Programming languages
Recursion
Recursive
Semantics
Software
Transformations
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively, and a weakest precondition semantics. Their equivalence is proved. A Hoare-like proof system for total correctness is also introduced and its soundness and completeness in an appropriate sense are shown. Finally, the recursion theoretic complexity of the notions introduced is studied. Admission of countable nondeterminism results in a lack of continuity of various semantic functions, and this is shown to be necessary for any semantics satisfying appropriate conditions. In proofs of total correctness, one resorts to the use of (countable) ordinals, and it is shown that all recursive ordinals are needed.
ISSN:0004-5411
1557-735X
DOI:10.1145/6490.6494