A new approach to program verification (Q2266579)

In this paper we have described a new methodology to verify a given program flowchart containing single loop or multiple nested loops by using the technique of mathematical induction. First the cut-points are created to cut loops in the given program flowchart. Then at these cut- points, the assertions and partial functions, which should be true for the given form of the program flowchart (may it be correct or incorrect), are proposed intuitively and then verified by applying the rule of mathematical induction. Finally these derived assertions and partial functions are utilised to decide definitely whether the given program flowchart is correct.