| An important feature of object-oriented programming languages is the ability to
dynamically instantiate user-defined container data structures such as lists, trees,
and hash tables. Programs implement such data structures using references to
dynamically allocated objects, which allows data structures to store unbounded
numbers of objects, but makes reasoning about programs more difficult. Reasoning
about object-oriented programs with complex data structures is simplified if data
structure operations are specified in terms of abstract sets of objects associated
with each data structure. For example, an insertion into a data structure in this
approach becomes simply an insertion into a dynamically changing set-valued field
of an object, as opposed to a manipulation of a dynamically linked structure linked
to the object.
In this paper we explore reasoning techniques for programs that manipulate data
structures specified using set-valued abstract fields associated with container objects.
We compare the expressive power and the complexity of specification languages
based on 1) decidable prefix vocabulary classes of first-order logic, 2) twovariable
logic with counting, and 3) Nelson-Oppen combinations of multisorted
theories. Such specification logics can be used for verification of object-oriented
programs with supplied invariants. Moreover, by selecting an appropriate subset
of properties expressible in such logic, the decision procedures for these logics yield
automated computation of lattice operations in abstract interpretation domain, as
well as automated computation of abstract program semantics. |