Title :
A New Verification Rule and Its Applications
Author_Institution :
Department of Computer Science, University of Houston
Abstract :
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.
Keywords :
Consistency; decomposition; invariant-relation theorem; loop program; predicate transformation; program verification; subgoal induction; verification rule; Computer science; Consistency; decomposition; invariant-relation theorem; loop program; predicate transformation; program verification; subgoal induction; verification rule;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1980.230788
