Graduate studies at Western
Minds and Machines 2 (3):283-307 (1992)
|Abstract||A proof of ‘correctness’ for a mathematical algorithm cannot be relevant to executions of a program based on that algorithm because both the algorithm and the proof are based on assumptions that do not hold for computations carried out by real-world computers. Thus, proving the ‘correctness’ of an algorithm cannot establish the trustworthiness of programs based on that algorithm. Despite the (deceptive) sameness of the notations used to represent them, the transformation of an algorithm into an executable program is a wrenching metamorphosis that changes a mathematical abstraction into a prescription for concrete actions to be taken by real computers. Therefore, it is verification of program executions (processes) that is needed, not of program texts that are merely the scripts for those processes. In this view, verification is the empirical investigation of: (a) the behavior that programs invoke in a computer system and (b) the larger context in which that behavior occurs. Here, deduction can play no more, and no less, a role than it does in the empirical sciences.|
|Keywords||Algorithms computers computer programs program executions (processes) program verification (‘correctness’ proofs, testing) representations (objects) software reliability|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Dan Klein & Christopher D. Manning, An Ç ´Ò¿ Μ Agenda-Based Chart Parser for Arbitrary Probabilistic Context-Free Grammars.
Robert F. Hadley (2008). Consistency, Turing Computability and Gödel's First Incompleteness Theorem. Minds and Machines 18 (1):1-15.
Ulrich Berger, Stefan Berghofer, Pierre Letouzey & Helmut Schwichtenberg (2006). Program Extraction From Normalization Proofs. Studia Logica 82 (1):25 - 49.
N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
Ildikó Sain (1988). Is “Some-Other-Time” Sometimes Better Than “Sometime” for Proving Partial Correctness of Programs? Studia Logica 47 (3):279 - 301.
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.
Timothy R. Colburn (1991). Program Verification, Defeasible Reasoning, and Two Views of Computer Science. Minds and Machines 1 (1):97-116.
James H. Fetzer (1988). Program Verification: The Very Idea. Communications of the ACM 31 (9):1048--1063.
Added to index2009-01-28
Total downloads6 ( #155,025 of 740,832 )
Recent downloads (6 months)0
How can I increase my downloads?