Theorem Generalization in Program Verification.

Abstract

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1981
Accession Number
ADA103749

Entities

People

  • Jan Vytopil
  • S. Kamal Abdali

Organizations

  • Rensselaer Polytechnic Institute

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Accumulators
  • Classification
  • Computations
  • Identities
  • Iterations
  • Language
  • Military Research
  • New York
  • Notation
  • Number Theory
  • Numbers
  • Specialization
  • Specifications
  • Standards
  • Theorems
  • Verification

Readers

  • Mathematical Modeling and Probability Theory.