Program verification,defeasible reasoning,and two views of computer science |
| |
Authors: | Timothy R Colburn |
| |
Affiliation: | (1) Department of Computer Science, University of Minnesota, 55812 Duluth, MN, USA |
| |
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: | Program verification program testing defeasible reasoning philosophy of computer science |
本文献已被 SpringerLink 等数据库收录! |
|