Thumbnail
Access Restriction
Subscribed

Author Apt, K. R. ♦ Plotkin, G. D.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1986
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract 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 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1986-08-10
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 33
Issue Number 4
Page Count 44
Starting Page 724
Ending Page 767


Open content in new tab

   Open content in new tab
Source: ACM Digital Library