COMPLETE AND CONSISTENT HOARE AXIOMATICS FOR A SIMPLE PROGRAMMING LANGUAGE

被引：9

作者：

CHERNIAVSKY, JC

KAMIN, SN

机构：

[1] Department of Computer Science, State University of New York, Stony Brook

来源：

JOURNAL OF THE ACM | 1979年 / 26卷 / 01期

关键词：

complexity; logic; programming languages; subrecurslve functions; theory of computation; venficatmn;

D O I：

10.1145/322108.322120

中图分类号：

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

学科分类号：

0812 ;

摘要：

A sunple programming language ffm IS defined for which a complete axiomatics is obtamable. Completeness is shown by presemmg a relauvely complete Hoare axiomatics, demonstrating, by direct constmcuon, that the first-order theory of addmon + as express,ve, and noting that + Is complete. It is then shown that m aS maxunal wath this property Further, a notton of complexity of a Hoare system is introduced based upon the lengths of proofs (dasregardmg proofs m the underlying logsc), and the system im,.+ is shown to have polynomial complexity The nouon ts shown to be nontnvlal by presenting a language for which any Hoare axiom system has exponenual complextty. © 1979, ACM. All rights reserved.

引用

页码：119 / 128

页数：10

共 12 条

[1]

Cherniavsky J. C., 1976, SIAM Journal on Computing, V5, P666, DOI 10.1137/0205045

[2]

CLARKE EM, 1977, 4TH P ACM S PRINC PR, P10

[3] SUBRECURSIVE PROGRAMMING LANGUAGES .1. EFFICIENCY AND PROGRAM STRUCTURE [J].

CONSTABLE, RL ;

BORODIN, AB .

JOURNAL OF THE ACM, 1972, 19 (03) :526-+

[4]

COOK SA, 1976, TR95 U TOR DEP COMPT

[5]

Cooper D. C., 1972, Machine intelligence 7, P91

[6]

Enderton H. B., 2001, MATH INTRO LOGIC, V2nd ed

[7]

Hoare C. A. R., 1973, Acta Informatica, V2, P335, DOI 10.1007/BF00289504

[8] EVEN SIMPLE PROGRAMS ARE HARD TO ANALYZE [J].

JONES, ND ;

MUCHNICK, SS .

JOURNAL OF THE ACM, 1977, 24 (02) :338-350

[9]

MANNA Z, 1974, MATH THEORY COMPUTAT

[10]

Mendelson E., 1964, INTRO MATH LOGIC

← 1 2 →