Intermittent-assertion method as a structural induction.
Karel Vosátka · Czech digital mathematics library · 1979
Method as a Structural Induction KAREL VOSATKA This paper formulates intermittent-assertion method for program verification as a structural induction.It analyses the inductive mechanism of the proof.The relation of the method to other known methods for program verification is studied.The paper also formulates verification conditions which represent the proof intermittent-assertion method.We shall show that the first type can be expressed by using subgoal induction method and then by using invariant method, too.What the IAM contributes to is just the second type of proofs.It is advantageous for the reader to know the paper [2], but it is not requirement. INTERMITTENT-ASSERTION METHODLet P be a program, J(x 0 ) be an input specification and K(x 0 , x) be an output specification, x is a program variable (or vector of variables) and x 0 is its input value.We are to prove the total correctness of program P with respect to J and K.We shall place cutpoints to the program P : at the entrance and at each exit of P and at least one inside of each loop.Intermittent assertion at some cutpoint A is written in the form: Sometime (At A and T(x))and it is read: "Sometime the computation is at the cutpoint A and T(x) holds."