SOCIAL PROCESSES AND PROOFS OF THEOREMS AND PROGRAMS

被引：204

作者：

DEMILLO, RA ^{[1
]}

LIPTON, RJ ^{[1
]}

PERLIS, AJ ^{[1
]}

机构：

[1] YALE UNIV,DEPT COMP SCI,NEW HAVEN,CT 06520

来源：

COMMUNICATIONS OF THE ACM | 1979年 / 22卷 / 05期

关键词：

formal mathematics; mathematical proofs; program specification; program verification;

D O I：

10.1145/359104.359106

中图分类号：

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

学科分类号：

0812 ;

摘要：

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design. © 1979, ACM. All rights reserved.

引用

页码：271 / 280

页数：10

共 22 条

[1] CHIEF PROGRAMER TEAM MANAGEMENT OF PRODUCTION PROGRAMMING
BAKER, FT
[J]. IBM SYSTEMS JOURNAL, 1972, 11 (01) : 56 - &
[2] BATEMAN P, 1978, MATH INTELLIGENCER, V1, P28
[3] INDEPENDENCE OF CONTINUUM HYPOTHESIS
COHEN, P
[J]. PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA, 1963, 50 (06) : 1143 - &
[4] INDEPENDENCE OF CONTINUUM HYPOTHESIS 2
COHEN, PJ
[J]. PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA, 1964, 51 (01) : 105 - &
[5] FIDELITY IN MATHEMATICAL DISCOURSE - IS ONE AND ONE REALLY TWO
DAVIS, PJ
[J]. AMERICAN MATHEMATICAL MONTHLY, 1972, 79 (03) : 252 - +
[6] Gelernter H. L., 1973, TOP CURR CHEM, V41, P113
[7] GEORGE JA, 1971, THESIS STANFORD U
[8] HEATH TL, 1956, 13 BOOKS EUCLIDS ELE, P204
[9] HOARE CAR, SOFTWARE MANAGEMENT
[10] JECH TJ, 1973, AXIOM CHOICE, P118

← 1 2 3 →