|
|
Abstract:
The problem of program verification has been discussed from a practical and a theoretical perspective. This debate seems very much alive. De Millo et al. have defined the agenda of the following debate. They claim that program verification is an impossible and an undesirable goal for computer science, because the community of computational scientist does not have an effective way to verify or accept theorems. Fetzer has proposed an answer to this article by making a distinction between programs and algorithms and by identifying the specification stage as the target of testing programs. This distinction is grounded in the dichotomy between causal processes and logical structures. Algorithms can be verified because of their logical nature, but programs, as long as they can be executed in a physical machine, have a causal character. We suggest that the distinction between program and algorithm could not been made in Fetzer's terms. An ontological division between programs and algorithms condemn the possibility of making any verification at all. Instead we propose that we can speak of causal and logical aspects when we are dealing with programs. This ontological deflation has as a consequence a redefinition of the testing target: the modeling process
|