Accession Number:

ADA043451

Title:

Verification Decidability of Presburger Array Programs.

Descriptive Note:

Interim rept.,

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1977-06-14

Pagination or Media Count:

22.0

Abstract:

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. The Presburger array theory, is defined, containing two logical sorts integer and array-of-integer. Addition, subtraction, and comparisons are permitted for integers. Array contents and assign functions, and, since the elements of the arrays are integers, array accesses may be nested. The first result is that the validity of unquantified formulas in Presburger array theory is decidable, yet quantified formulas in general are undecidable.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE