The First-Order Theory of Sets with Cardinality Constraints is Decidable

Data structures often use an integer variable to keep track of the number of elements they store. An invariant of such data structure is that the value of the integer variable is equal to the number of elements stored in the data structure. Using a program analysis framework ports abstraction of data structures as sets, such constraints can be expressed using the language of sets with cardinality constraints. The same language can be used to express preconditions that guarantee the correct use of the data structure interfaces, and to express invariants useful for the analysis of the termination behavior of programs that manipulate objects stored in data structures. In this paper we show the decidability of valid formulas in one such language. Specifically, we examine the first-order theory that combines 1) Boolean algebras of sets of uninterpreted elements and 2) Presburger arithmetic operations. Our language allows relating the cardinalities of sets to the values of integer variables...

• Type: Journal
• Year: 2004
• Where: CORR
• Authors: Viktor Kuncak, Martin C. Rinard
• Keywords: CORR 2004, Data Structures, Education, Integer Variables, Uninterpreted Elements