SYNTACTIC AND SEMANTIC DEPENDENCE OF ARRAY-ARITHMETIC SENTENCES, WITH AN APPLICATION TO PROGRAM VERIFICATION

Article type: Research Article

Authors: Marcus, Leo

Affiliations: Computer Systems Division, The Aerospace Corporation, P.O. Box 92957. Los Angeles. CA 90009, USA. E-mail: marcus@aero.org

Abstract: We present an algorithm that takes a first-order sentence φ in full arithmetic with arrays (with quantification over numbers, and with numerical terms serving as array indices), and builds a test formula that can be used to determine which indices of φ's constituent arrays “really” occur. We call this concept syntactic dependence. We show how to use syntactic dependence as a test for semantic dependence, i.e., the true dependence of φ on the value of an array element. This is useful in truth-maintenance systems or symbolic execution systems, where a sentence may be true in one state but false in the next. More specifically, if we are given an initial state, a sentence (such as φ above) that is true in the initial state, and a list of array elements that may be changing value during a state transition, the algorithm can be used to determine whether φ must remain true after the state transition.

DOI: 10.3233/FI-1996-27105

Journal: Fundamenta Informaticae, vol. 27, no. 1, pp. 77-100, 1996