Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CORR

2004

Springer

2004

Springer

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...

Related Content

Added |
17 Dec 2010 |

Updated |
17 Dec 2010 |

Type |
Journal |

Year |
2004 |

Where |
CORR |

Authors |
Viktor Kuncak, Martin C. Rinard |

Comments (0)