Simple Programs Realize Exactly Presburger Formulas

Abstract

A class of programs, $L_ + $, is introduced which lies between $L_1 $ and $L_2 $ in the loop program hierarchy. As a tool for analysis of this class, we use formulas in Presberger’s arithmetic and we show that $L_ + $ realizes these formulas both relationally and functionally. Moreover, the realization is exact in the sense that every program in $L_ + $ realizes some Presberger formula. Using known decidability and complexity results for Presberger's arithmetic, we are able to obtain a decision procedure for equivalence of $L_ + $ programs and to obtain upper bounds for the complexity of this procedure.