Theorem Generalization in Program Verification.
Jan Vytopil, S. Kamal Abdali · Defense Technical Information Center (DTIC) · 1981
The generalization of theorems about programs obtained from recursive schemas is discussed. Methods are given to generalize theorems about two classes of programs to make the theorems easier to prove by induction. Invariant assertions are obtained as a by-product of the generalization process. Also, methods are given to redefine the functions representing programs so as to simplify the proof of programs properties in certain cases. (Author)