Synthesis of Invariant Assertions for Arithmetical Programs.
Abstract
A program is called arithmetical if it is obtained from a flowchart schema under an interpretation in which the domain consists of non-negative integers and the assigned functions and predicates are arithmetical in the sense of Goedel. The computation done by arithmetical programs is characterized in terms of arithmetical predicates. This is a first-order formalization, compared to the second-order, Cooper-Manna formalization. It is shown that for the class of arithmetical programs, the problem of synthesis of invariant assertions is solvable, and a simple algorithm is given to construct arithmetic predicates which can serve as invariant assertions. Two alternative definitions of invariant assertions found in the literature -- minimal predicates and optimal predicates -- are shown to be equivalent. It is proved that the arithmetical predicates generated by our algorithm satisfy the definition of both minimal and optimal predicates. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1981
- Accession Number
- ADA103748
Entities
People
- Jan Vytopil
- S. Kamal Abdali
Organizations
- Rensselaer Polytechnic Institute