Philosophy of Computer Science
Can Programs Be Verified?
Last Update: 11 September 2012
Note:
or
material is highlighted
|
"I hold the opinion that the construction of computer programs is a
mathematical activity like the solution of differential equations,
that programs can be derived from their specifications through
mathematical insight, calculation, and proof, using algebraic laws
as simple and elegant as those of elementary arithmetic."
"Computer programming is an exact science in that all the properties of
a program and all the consequences of executing it in any given
environment can, in principle, be found out from the text of the
program itself by means of purely deductive reasoning."
"When the correctness of a program, its compiler, and the hardware
of the computer have all been established with mathematical
certainty, it will be possible to place great reliance on the
results of the program, and predict their properties with a
confidence limited only by the reliability of the
electronics."—C.A.R. Hoare
-
Turing, Alan M.
(1949),
"Checking a Large Routine",
in Report of a Conference on High Speed Automatic Calculating
Machines
(Cambridge, UK: University Mathematics Lab): 67-69.
- Reprinted in:
Morris, F.L.,
& Jones, C.B.
(1984),
"An Early Program Proof by Alan Turing",
Annals of the History of Computing
6(2) (April): 139-143.
-
McCarthy, John (1963), "Towards a Mathematical Science of
Computation", in C.M. Popplewell (ed.), Information Processing
1962: Proceedings of DFIP Congress 62 (Amsterdam:
North-Holland): 21-28; reprinted
in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 35-56.
-
Naur, Peter (1966), "Proof of Algorithms by General Snapshots",
BIT 6: 310-316; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 57-64.
-
Floyd, Robert W. (1967), "Assigning Meanings to Programs", in
Mathematical Aspects of Computer Science: Proceedings of Symposia in
Applied Mathematics, Vol. 19 (American Mathematical Society): 19-32;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 65-81.
-
Hoare, C.A.R. (1969), "An Axiomatic Basis for Computer
Programming", Communications of the ACM 12: 576-580, 583;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 83-96.
- Hoare, C.A.R. (1986), "Mathematics of Programming", Byte
(August); reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 135-154.
-
Shustek, Len (ed.),
"An Interview with C.A.R. Hoare",
Communications of the ACM
52(3) (March): 38-41.
-
Hoare, C.A.R.
(2009),
"Retrospective: An Axiomatic Basis for Computer Programming",
Communications of the ACM
52(10) (October): 30-32.
-
Humelsine, Jim (2010),
"Software Still as Much an Art as Science",
Letters to the Editor,
Communications of the ACM
53(1) (January): 7;
doi:10.1145/1629175.1629178
-
Dijkstra, Edsgar W.
(1974),
"Programming as a Discipline of Mathematical Nature",
American Mathematical Monthly
(June-July): 608-612.
-
Dijkstra, Edsgar W.
(1975),
"Guarded Commands, Nondeterminacy and Formal Derivation of Programs",
Communications of the ACM 18(8): 453-457
-
De Millo, Richard A.; Lipton, Richard J.; & Perlis, Alan J. (1979),
"Social
Processes and Proofs of Theorems and Programs",
Communications of the ACM 22(5): 271-280; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 297-319.
- Naur, Peter (1982), "Formalization in Program Development",
BIT 22: 437-453; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 191-210.
- Dijkstra, Edsger W. (1983),
"Fruits of Misunderstanding" (EWD-854),
reprinted in Datamation (15 February 1985): 86-87.
- Scherlis, William L.; & Scott, Dana S. (1983), "First Steps towards
Inferential Programming", in R.E.A. Mason (ed.), Information
Processing 83 (JFIP and Elsevier Science Publishers): 199-212;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 99-133.
- Olson, Steve (1984, January/February), "Sage of Software",
Science: 75-80.
-
Gries, David (1981),
The
Science of Programming (New York:
Springer-Verlag).
- Meyer, Bertrand (1985), "On Formalism in Specifications", IEEE
Software 2(1) (January): 6-26; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 155-189.
-
Smith, Brian Cantwell (1985),
"Limits of Correctness in Computers",
ACM SIGCAS Computers and Society
14-15 (1-4) (January): 18–26;
also published as:
Technical Report CSLI-85-36 (Stanford, CA: Center for the Study
of Language and Information);
reprinted
in Charles Dunlop & Rob Kling (eds.), Computerization and
Controversy
(San Diego: Academic Press, 1991): 632–646; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 275–293.
-
Also see:
Fetzer, James H. (1999),
"The
Role of Models in Computer Science" [PDF],
The Monist
82(1):
20-36.
-
Also possibly of relevance:
Jackson, Michael (2003),
"Why Software Writing Is Difficult and Will Remain So" [PDF],
Information Processing Letters
88: 13-25.
-
For more examples like Smith's moon-mistaken-as-missile,
only with more dire consequences, see:
Neumann, Peter G. (1993),
"Modeling and Simulation",
Communications of the ACM
36(4) (June): 124.
-
Another interesting article on computational modeling (and
what can go wrong):
Hayes, Brian (2007),
"Calculating the Weather",
American Scientist 95(3) (May-June): 271-273.
-
On the nature of abstraction, see:
-
Rapaport, William J. (1999),
"Implementation Is Semantic Interpretation" [PDF],
The Monist
82
(1):
109-130.
-
Kramer, Jeff (2007),
"Is Abstraction the Key to Computing?",
Communications of the ACM
50(4) (April): 36-42.
-
Dewar, Robert (2009),
"CS Education in the U.S.:
Heading in the Wrong Direction?",
Communications of the ACM
52(7) (July): 41–43.
-
Morrisett, Greg (2009),
"A Compiler's Story",
Communications of the ACM
52(7) (July): 106.
- Verity, John W. (1985), "Bridging the Software Gap", Datamation
(15 February): 84, 88.
-
Myers, Ware (ed.) (1986),
"Can Software for the Strategic Defense Initiative Ever Be Error-Free?",
[IEEE] Computer
(November): 61–67.
- Floyd, Christiane (1987), "Outline of a Paradigm Change in Software
Engineering", in G. Bjerknes et al. (eds.), Computers and
Democracy: A Scandinavian Challenge (Brookfield, VT: Gower
Publishing): 191-210; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 239-259.
-
Fetzer, James H. (1988),
"Program Verification: The Very Idea",
Communications of the ACM 31(9) (September): 1048-1063;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 321-358.
- Ardis, Mark; Basili, Victor; Gerhart, Susan; Good, Donald; Gries,
David; Kemmerer, Richard; Leveson, Nancy; Musser, David; Neumann,
Peter; & von Henke, Friedrich (1989),
"Editorial
Process
Verification" (letter to the editor, with replies by James H. Fetzer
and Peter J. Denning), ACM Forum, Communications of the ACM
32(3) (March): 287-290.
- Pleasant, James C.; AND Paulson, Lawrence; Cohen, Avra; & Gordon,
Michael; AND Bevier, William R.; Smith, Michael K.; & Young, William
D.; AND Clune, Thomas R.; AND Savitzky, Stephen (1989),
"The Very
Idea" (5 letters to the editor), Technical Correspondence, Communications of the ACM 32(3) (March): 374-377.
- Fetzer, James H. (1989),
"Program
Verification Reprise: The Author's
Response" (to the above 5 letters), Technical Correspondence, Communications of the ACM 32(3) (March): 377-381.
- Dobson, John; & Randell, Brian (1989),
"Program Verification: Public
Image and Private Reality", Communications of the ACM 32(4)
(April): 420-422.
- Müller, Harald M.; AND Holt, Christopher M.; AND Watters, Aaron
(1989),
"More on the Very Idea" (3 letters to the editor, with reply
by James H. Fetzer), Technical Correspondence, Communications of the ACM 32(4) (April): 506-512.
- Hill, Richard; AND Conte, Paul T.; AND Parsons, Thomas W.; AND Nelson,
David A. (1989),
"More on Verification" (4 letters to the editor),
ACM Forum, Communications of the ACM 32(7) (July): 790-792.
- Tompkins, Howard E. (1989),
"Verifying Feature-Bugs" (letter to the
editor), Technical Correspondence, Communications of the ACM 32:
1130-1131.
-
Note: This does not seem to be available on-line.
-
Barwise, Jon (1989),
"Mathematical
Proofs of Computer System Correctness" [PDF],
Notices of the American Mathematical Society
36: 844-851.
Included in the online version of the above:
- Dudley, Richard (1990), "Program Verification" (letter to Jon Barwise
(ed.), Computers and Mathematics column, with a reply by Barwise), Notices of the American Mathematical Society 37: 123-124.
- Fetzer, James H. (1991), "Philosophical Aspects of Program
Verification", Minds and Machines 1: 197-216; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 403-427.
- Fetzer, James H. (1993), "Program Verification", in Allen Kent &
James G. Williams
(eds.),
Encyclopedia of Computer Science and
Technology, Vol. 28, Supp. 13 (New York: Marcel Dekker): 237-254;
reprinted in
Allen Kent &
James G. Williams (eds.), Encyclopedia of Microcomputers,
Vol. 14: Productivity and Software Maintenance: A Managerial
Perspective to Relative Addressing (New York: Marcel Dekker): 47-64.
-
Fetzer, James H. (1998),
"Philosophy and Computer Science:
Reflections on the Program Verification Debate", in
Bynum, Terrell Ward; & Moor, James H. (eds.),
The Digital Phoenix:
How Computers Are Changing Philosophy, Revised Edition
(Oxford: Blackwell): 253-273.
- Fetzer, James H. (1996), "Computer Reliability and Public Policy:
Limits of Knowledge of Computer-Based Systems", Social Philosophy
and Policy, forthcoming.
- Blum, Bruce I. (1989), "Formalism and Prototyping in the Software
Process", Information and Decision Technologies 15: 327-341;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 213-238.
- Cohen, Avra (1989), "The Notion of Proof in Hardware Verification",
Journal of Automated Reasoning 5: 127-139; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 359-374.
- Colburn, Timothy R. (1991), "Program Verification, Defeasible
Reasoning, and Two Views of Computer Science", Minds and
Machines 1: 97-116; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 375-399.
- Devlin, Keith (1992), "Computers and Mathematics", Notices of the
American Mathematical Society 39: 1065-1066.
- MacKenzie, Donald (1992), "Computers, Formal Proofs, and the Law
Courts", Notices of the
American Mathematical Society 39: 1066-1069.
- Naur, Peter (1992), "The Place of Strictly Defined Notation in Human
Insight", in Computing: A Human Activity (Addison-Wesley);
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 261-274.
- Nelson, David A. (1992), "Deductive Program Verification (A
Practitioner's Commentary)", Minds and Machines 2: 283-307.
- Colburn, Timothy R. (1993), "Computer Science and Philosophy", in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers): 3-31.
- Colburn, Timothy R.; Fetzer, James H.; & Rankin, Terry L. (eds.)
(1993), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers).
- contains a lengthy bibliography
- Nelson, David A. (1993), Review of Boyer & Moore's A
Computational Logic Handbook and Moore's Special Issue on System
Verification (Journal of Automated Reasoning), in Minds and
Machines 4: 93-101.
- Bowen, J.P., & Hinchey, M.G. (1995), "Ten Commandments of Formal Methods",
IEEE Computer 28(4): 56-63.
- Glanz, James (1995), "Mathematical Logic Flushes Out the Bugs in Chip
Designs", Science 267: 332-333.
-
Neumann, Peter (1996, July),
"Using
Formal Methods to Reduce Risks",
Communications of the ACM
39(7): 114.
- Pollack, Andrew (1999, May 3), "For Coders, a Code of Conduct: 2000 Problem
Tests Professionalism of Programmers", The New York Times: C1, C12.
-
Hinchey, Mike;
Jackson, Michael;
Cousot, Patrick;
Cook, Byron;
Bowen, Jonathan P.;
&
Margaria, Tiziana
(2008),
"Software Engineering and Formal Methods",
Communications of the ACM
51(9) (September): 54-59.
- A recent statement of the argument in favor of program
verification.
-
Clarke, Edmund M.;
Emerson, E. Allen;
&
Sifakis, Joseph
(2010),
"Model Checking:
Algorithmic Verification and Debugging",
Turing Lecture,
Communications of the ACM
52(11) (November): 74–84.
Copyright © 2004–2012 by
William J. Rapaport
(rapaport@buffalo.edu)
http://www.cse.buffalo.edu/584/canprogsbeverified.html-20120911