Synthesis of Invariant Assertions for Arithmetical Programs

摘要

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)