Program verification, defeasible reasoning, and two views of computer science
Minds and Machines 1 (1) (1991)
| Abstract | In this paper I attempt to cast the current program verification debate within a more general perspective on the methodologies and goals of computer science. I show, first, how any method involved in demonstrating the correctness of a physically executing computer program, whether by testing or formal verification, involves reasoning that is defeasible in nature. Then, through a delineation of the senses in which programs can be run as tests, I show that the activities of testing and formal verification do not necessarily share the same goals and thus do not always constitute alternatives. The testing of a program is not always intended to demonstrate a program's correctness. Testing may seek to accept or reject nonprograms including algorithms, specifications, and hypotheses regarding phenomena. The relationship between these kinds of testing and formal verification is couched in a more fundamental relationship between two views of computer science, one properly containing the other. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | No categories specified (fix it) | |||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,672 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesG. Aldo Antonelli (2005). Grounded Consequence for Defeasible Logic. Cambridge University Press.
Amnon H. Eden (2007). Three Paradigms of Computer Science. Minds and Machines 17 (2).
Edward Yalow (1977). Yaq: A 360 Assembler Version of the Algorithm Aq and Comparison with Other Pl/I Programs. Department of Computer Science, University of Illinois at Urbana-Champaign.
Gordon McCabe (2005). Universe Creation on a Computer. Studies in History and Philosophy of Science Part B 36 (4):591-625.
James H. Fetzer (1991). Philosophical Aspects of Program Verification. Minds and Machines 1 (2):197-216.
N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
Alan W. Richardson (1992). Philosophy of Science and Its Rational Reconstructions: Remarks on the VPI Program for Testing Philosophies of Science. PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1992:36 - 46.
Robert L. Causey (2003). Computational Dialogic Defeasible Reasoning. Argumentation 17 (4):421-450.
David A. Nelson (1992). Deductive Program Verification (a Practitioner's Commentary). Minds and Machines 2 (3).
James H. Fetzer (1988). Program Verification: The Very Idea. Communications of the ACM 31 (9):1048--1063.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads21 ( #58,715 of 549,067 )Recent downloads (6 months)1 ( #63,185 of 549,067 )How can I increase my downloads? |
My notes
Discussion
