COUNTABLE NONDETERMINISM AND RANDOM ASSIGNMENT

被引：86

作者：

APT, KR ^{[1
]}

PLOTKIN, GD ^{[1
]}

机构：

[1] UNIV EDINBURGH,DEPT COMP SCI,EDINBURGH EH9 3JZ,MIDLOTHIAN,SCOTLAND

来源：

JOURNAL OF THE ACM | 1986年 / 33卷 / 04期

关键词：

COMPUTER METATHEORY;

D O I：

10.1145/6490.6494

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：724 / 767

页数：44

共 35 条

[1]

ACZEL P, 1977, N HOLLAND STUDIES LO, V90, P739

[2]

Apt K.R., 1974, ANN MATH LOGIC, V6, P177, DOI [10.1016/0003-4843(74)90001-1, DOI 10.1016/0003-4843(74)90001-1]

[3] 10 YEARS OF HOARE LOGIC - A SURVEY .2. NONDETERMINISM [J].

APT, KR .

THEORETICAL COMPUTER SCIENCE, 1984, 28 (1-2) :83-109

[4] PROOF RULES AND TRANSFORMATIONS DEALING WITH FAIRNESS [J].

APT, KR ;

OLDEROG, ER .

SCIENCE OF COMPUTER PROGRAMMING, 1983, 3 (01) :65-100

[5] 10 YEARS OF HOARE LOGIC - A SURVEY .1. [J].

APT, KR .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1981, 3 (04) :431-483

[6]

APT KR, 1981, LECTURE NOTES COMPUT, V115, P479

[7]

BACK RJ, 1980, LECTURE NOTES COMPUT, V85, P51

[8] PROVING TOTAL CORRECTNESS OF NONDETERMINISTIC PROGRAMS IN INFINITARY LOGIC [J].

BACK, RJR .

ACTA INFORMATICA, 1981, 15 (03) :233-249

[9] A CONTINUOUS SEMANTICS FOR UNBOUNDED NONDETERMINISM [J].

BACK, RJR .

THEORETICAL COMPUTER SCIENCE, 1983, 23 (02) :187-210

[10]

BERRY G, 1985, 1982 P FRENCH SEM AP

← 1 2 3 4 →