Program verification, defeasible reasoning, and two views of computer science

Research output: Contribution to journalArticle

3 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)97-116
Number of pages20
JournalMinds and Machines
Volume1
Issue number1
DOIs
StatePublished - Feb 1 1991

Keywords

  • Program verification
  • defeasible reasoning
  • philosophy of computer science
  • program testing

Fingerprint Dive into the research topics of 'Program verification, defeasible reasoning, and two views of computer science'. Together they form a unique fingerprint.

  • Cite this