Discovering Properties about Arrays in Simple Programs

Array bound checking and array dependency analysis (for par-allelization) have been widely studied. However, there are much less results about analyzing properties of array contents. In this paper, we propose a way of using abstract interpreta-tion for discovering properties about array contents in some restricted cases: one-dimensional arrays, traversed by simple “for ” loops. The basic idea, borrowed from [15], consists in partitioning arrays into symbolic intervals (e.g., [1, i−1], [i, i], [i + 1, n]), and in associating with each such interval I and each array A an abstract variable AI; the new idea is to con-sider relational abstract properties ψ(AI, BI,...) about these abstract variables, and to interpret such a property pointwise on the interval I: ∀ ` ∈ I, ψ(A[`], B[`],...). The abstract se-properties has been defined and implemented in a prototype tool. The method is able, for instance, to discover that the re-sult of an insertion sort is a sorted array, or that, in an array traversal guarded by a “sentinel”, the index stays within the bounds.