Issue No.05 - September (1980 vol.6)
J.C. Huang , Department of Computer Science, University of Houston
This paper describes a verification rule for loop programs, and shows how it can be used in conjunction with the invariant-relation theorem to facilitate verification of programs.
verification rule, Consistency, decomposition, invariant-relation theorem, loop program, predicate transformation, program verification, subgoal induction
J.C. Huang, "A New Verification Rule and Its Applications", IEEE Transactions on Software Engineering, vol.6, no. 5, pp. 480-484, September 1980, doi:10.1109/TSE.1980.230788