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. Huang, "A New Verification Rule and Its Applications," in IEEE Transactions on Software Engineering, vol. 6, no. , pp. 480-484, 1980.