Verification Decidability of Presburger Array Programs

A program annotated with inductive assertions is said to be verification decidable If all of the verification conditions generated from the program and assertions are formulas In a decidable theory A theory is defined, which is called Presburger array theory, containing two logical sorts integer and array of integer Addltmn, subtraction, and comparisons are permztted for integers Array access and assignment functmns are allowed Since the elements of the arrays are integers, array accesses may be nested First, it is observed that the validity of unquantlfied formulas in Presburger array theory is decidable, yet quantified formulas in general are undecldable It is then shown that, with certain restrictions, one can add a new predicate Perm(M, N)--meanlng array M is a permutation of array N--to the assertion language and still have a solvable decision problem for verification conditions generated from unquantified assertions The significance of this result is that almost all known one-array sorting programs are verlticatmn decidable when annotated with inductive assertions for proving that the output is a permutation of the input