Abstract
Proving the correctness of a program involves generating mathematical formulae, known as verification conditions, and then proving that these hold. The two basic methods of generating verification conditions are known as forward accumulation and back substitution. This paper describes a new method, the modification index (MX) method, which has certain advantages over both forward accumulation and back substitution.
In the MX method, the variables of the program are no longer the verification variables (those occurring in verification conditions). Each verification variable consists of a program variable with a modification index appended. Thus if V is a program variable, then V0, V1, V2, and so on, may be the verification variables, where the small integer (0, 1, 2, and so on) is the modification index.
We analyze one path at a time. In a given path we have an initial assertion (associated with the start of the path), certain assignments, conditions, and restrictions, and a final assertion (associated with the end of the path). The initial value of V in this path may be denoted by V0; if V changes (by means of an assignment, subroutine call, side effect, etc.), the new values of V in this path are V1, V2, and so on.
We have described the MX method as a forward method, but in fact it is a directionless method; we could just as easily have numbered the modification indices in reverse order, with V0 corresponding to the final value of V instead of the initial value. If we do this, we get an immediate proof that the MX method is equivalent to back substitution; if we leave the indices in forward order, we get an immediate proof that the MX method is equivalent to forward accumulation. But the MX values could be chosen arbitrarily (without regard to order), without affecting the validity of the MX method.
The advantages of the MX method are as follows. First, no symbolic values are kept, and no symbolic algebraic manipulation is done; we need only keep a table of the MX of every variable. Second, the verification conditions of even a complex path can now be immediately read off "by hand" from the path, without computer aid. Third, in many cases the verification conditions produced by the MX method are less bulky than those produced by forward acccumulation or back substitution; in all cases, we can easily transform the verification conditions produced by the MX method into a form which is never bulkier than the result of applying the forward accumulation method.
