Stopping conditions, verification

We assume that we are given a flowchart scheme P and a path a in P. This path may be from START to STOP or it may be from any statement in P to any other statement in P. We assume that we are given an initial predicate A and final predicate B. We wish to construct mechanically - i.e. by an algorithm which can be implemented on a computer - a VERIFICATION CONDITION V(P,a,A,B) with the following property. We assune now that input variables X and program variables Y are disjoint. 

If the flowchart P has a loop-free graph - if P is a tree - then the construction of W(P,A,B) is now quite simple. If P is loop-free there are only a finite number of paths 0, ...,on from START to STOP which are consistent and hence execution sequences. The input condition A(X) is a function only of the inputs, of course, while the output condition B(X,Y) can be regarded as a function of the input and of the final values of all the program variables (some of these values, of course, may play no role in the statement of the condition). Notice that under these conditions, when is a complete execution sequence from START to STOP, the path verification condition VCPjO AB, ) for any interpretation I is a function of the input X alone. 

We wish to see that for any choice of X = a and Y = b each path verification condition in W(P,A,B,I) holds. That is, we must examine each V(P,a,At r,I)(a,b) where o is a consistent path from tagged point t to tagged point r not passing through any other tagged point en route from t to r. If the hypothesis of the conditional expression V(P,a,A, A r,I)(a,b) is false, then the verification condition is vacuously true. If it is true, then A (a,b) is true and by definition of Aj, A(a) is true and computation (P,I,a) at some point enters tagged point t with Y = b. Further a is the continuation of this computation and reaches r with Y = b. So there is certainly a time when computation (P,I,a) reaches r with this specification of Y. Now if r is not a STOP statement, inductive assertion was assigned by our definition and thus Ar(a,b ) holds by definition. 

There are 7 paths to verify one from START to STOP not passing through a, one from START to a, one from a to B, one from a to STOP and two from 0 back to B and one from S up to a. (Why is there no need to verify the path for which DIMENSION X(N) is false ) We leave It to the reader to check out these path verification conditions. 

---