Proof and Validation of Program Correctness

McCarthy (1962) suggested that programs should be proved correct rather than merely verified and considerable effort has since gone into the study of techniques for so doing (McCarthy and Painter, 1967; Floyd, 1967; Cooper, 1968; Burstall, 1969). McCarthy and Painter (1967) proved the correctness of a compiler for certain arithmetic expressions, Burstall (1969) proved that a tree sort program was correct and recently London (1970) has proved the correctness of a number of ALGOL procedures; however, little progress has been made in using mathematical deductive techniques to devise methods directly applicable to the majority of practical programs. Algebraic inductive methods of program analysis have been developed which lead to advances in programming languages and the theory of algorithms; graph theoretical techniques of flowchart interpretation have also been developed and used, which have advanced algorithm and system theory. Both these approaches have contributed to understanding the theory of programming and have also contributed to the mathematical theory of computation. However, we must ask whether these techniques are in fact making progress towards proving that programs are correct, also what it means to prove that a program is correct, whether there is any possibility of doing so, and whether we want to do so anyway. McCarthy's argument is based on the assertion that a mathematical theory of computation ought to exist and that such a theory should lead to programs being proved correct, just as theorems in mathematics are proved true. The proof of a mathematical theorem 0 is essentially the demonstration that the theorem is the logical inference from a set of axioms {Ai\i = 1,2,.. . , «},i.e. Al AA2 A . . . AAn => 0 takes the value Tfor all interpretations in a non-empty universe. In proving the correctness of computer programs we have to define the term correctness. It has been defined by Manna (1969); viz., 'A program is said to be correct if its execution terminates and yields the desired results.' Whilst not disputing this definition it seems to beg for further definition of the 'desired results'. In carrying out certain mathematical tasks we may be able to specify the desired results (whether we execute the task on a computer or not) and so we may prove the correctness of a procedure. This is not the case, however, in many common applications of computers such as scheduling, sales forecasting, production control or simulation. In fact it appears that in general we cannot even specify what, for a particular task, the desired results are, and we certainly cannot make a specification sufficiently precisely to satisfy the determination of any first order formula. Hence we cannot prove the correctness of programs in the mathematical sense as suggested by McCarthy, more due to our inability to state what we are trying to prove than to our inability to find actual proof methods. If such an approach to program validation fails then we must look for other techniques by which we can reduce program errors and increase our confidence in a program. Let us analyse the nature of a program. Firstly, we can consider a program to be an abstract construction engineered in a similar fashion to a physical construction. In this case we test or validate the program using statistical principles of quality control. This is the basis of most program validation currently performed and, although much is achieved by this technique, as practised, it falls short of what is required. Secondly, we can think of a program as a strictly deterministic mathematical procedure and prove its correctness, but as we have seen, this appears to be too narrow a conceptual interpretation of a program and we cannot prove correctness except in special cases. A third interpretation of a program, as a form of automaton, is a useful basis for discussion. If, given some input, a given program terminates and produces some output, we say it is a legal program. Now, instead of trying to prove that the output is that desired, we try to determine the expected output. This amounts to determining for what purpose the program is correct, rather than trying to prove that the program itself is correct. Suppose for some given program, P, we have a specification consisting of a listing representing the procedure. We divide the set of all possible inputs into subsets, each being distinguished by the property that all elements within the subset will be treated similarly by the program. Each subset will be input to the program in the form of a string. We now determine whether, given some input string /,(«„ a2, a3, . . ., ani), the program terminates and produces an output. If this is the case we have a legal program and can proceed further to determine that P acting on some Instantiation of/, will result in a corresponding instantiation of the output Jl. i.e. Va,, a2, a3, . . ., a^PI^ => /,(a,, cc2,. . ., ami) This does not, however, prove that P is correct; we have also to determine the output resulting from other possible input strings 72, 73, . .., Ik so obtaining a specification of the program, viz. Va,, a2,. . ., ani PI^u a2, > «„,) => Afci, a2, • • ., ami) Va,, a2,.. ., ani PI2(au a2,. . ., ani) => J2(xu a 2 , . . ., am2) Va,, a 2 , . . ., ank PIk(at, a2,. . ., ani) => Jk(ccu

ReadCiteExport

Add to List

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Sign up to Zendy

Having issues? You can contact us here