APPLICATION OF VERIFICATION METHOD AND A DECOMPOSITION METHOD TO PROGRAM MODIFICATION

This paper considers the case where the specification and the program are modified. A method is proposed that specifies the range which is a ffected by the modification using the verification method and decompos ition technique. By the proposed technique, the points where the modif ication is required or the point which may contain an error can be est imated when the program is modified. The inductive assertion is used a s the verification technique. It is assumed that the specification bef ore modification as well as the program are already verified for the c orrectness. The object of verification is simplified by the comparison and validation of the verification history and the object of correctn ess verification. The part which is left without being simplified is t he range affected by the modification before the comparison and after the correctness verification, the rage which is affected by the modifi cation as well as the range for which the validation is not satisfies can be specified.