Advertisement

CSL 2010: Computer Science Logic pp 34-48

# Ordered Sets in the Calculus of Data Structures

• Viktor Kuncak
• Ruzica Piskac
• Philippe Suter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6247)

## Abstract

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of constraints in a modular way, by combining multiple decidable classes. Working with quantifierfree combinations of constraints makes the combination agenda more realistic and the resulting logics more likely to be tractable than in the presence of quantifiers.

Our approach to combination is based on reducing decidable fragments to a common class, Boolean Algebra with Presburger Arithmetic (BAPA). This logic was introduced by Feferman and Vaught in 1959 and can express properties of uninterpreted sets of elements, with set algebra operations and equicardinality relation (consequently, it can also express Presburger arithmetic constraints on cardinalities of sets). Combination by reduction to BAPA allows us to obtain decidable quantifierfree combinations of decidable logics that share BAPA operations. We use the term Calculus of Data Structures to denote a family of decidable constraints that reduce to BAPA. This class includes, for example, combinations of formulas in BAPA, weak monadic second-order logic of k-successors, two-variable logic with counting, and term algebras with certain homomorphisms. The approach of reduction to BAPA generalizes the Nelson-Oppen combination that forms the foundation of constraint solvers used in software verification. BAPA is convenient as a target for reductions because it admits quantifier elimination and its quantifier-free fragment is NP-complete.

We describe a new member of the Calculus of Data Structures: a quantifier-free fragment that supports 1) boolean algebra of finite and infinite sets of real numbers, 2) linear arithmetic over real numbers, 3) formulas that can restrict chosen set or element variables to range over integers (providing, among others, the power of mixed integer arithmetic and sets of integers), 4) the cardinality operators, stating whether a given set has a given finite cardinality or is infinite, 5) infimum and supremum operators on sets. Among the applications of this logic are reasoning about the externally observable behavior of data structures such as sorted lists and priority queues, and specifying witness functions for the BAPA synthesis problem. We describe an abstract reduction to BAPA for our logic, proving that the satisfiability of the logic is in NP and that it can be combined with the other fragments of the Calculus of Data Structures.

## Keywords

Boolean Algebra Decision Procedure Cardinality Constraint Binary Search Tree Integer Linear Programming Problem
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

1. [ES06]
Eisenbrand, F., Shmonin, G.: Carathéodory bounds for integer cones. Operations Research Letters 34(5), 564–568 (2006), http://dx.doi.org/10.1016/j.orl.2005.09.008
2. [FV59]
Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundamenta Mathematicae 47, 57–103 (1959)
3. [Ghi05]
Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning 33(3-4), 221–249 (2005)
4. [GHN+04]
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)Google Scholar
5. [KMPS10]
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)Google Scholar
6. [KNR06]
Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning (2006)Google Scholar
7. [KPSW10]
Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 26–44. Springer, Heidelberg (2010)
8. [KR07]
Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007)
9. [Lae68]
Laeuchli, H.: A decision procedure for the weak second order theory of linear order. Studies in Logic and the Foundat. of Math. 50, 189–197 (1968)
10. [MW80]
Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980)
11. [OSV08]
Odersky, M., Spoon, L., Venners, B.: Programming in Scala: a comprehensive step-by-step guide. Artima Press (2008)Google Scholar
12. [PH05]
Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information 14(3), 369–395 (2005)
13. [PK08a]
Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 218–232. Springer, Heidelberg (2008)
14. [PK08b]
Piskac, R., Kuncak, V.: Fractional collections with cardinality bounds. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 124–138. Springer, Heidelberg (2008)
15. [PK08c]
Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 268–280. Springer, Heidelberg (2008)
16. [PST00]
Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first-order two-variable logic with counting. SIAM J. on Computing 29(4), 1083–1117 (2000)
17. [Rab69]
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)
18. [Ram30]
Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc. s2-30, 264–286 (1930), doi:10.1112/plms/s2-30.1.264Google Scholar
19. [RRZ05]
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 48–64. Springer, Heidelberg (2005)
20. [SDK10]
Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL (2010)Google Scholar
21. [She75]
Shelah, S.: The monadic theory of order. The Annals of Mathematics of Mathematics 102(3), 379–419 (1975)
22. [SS07]
Sofronie-Stokkermans, V.: Hierarchical and modular reasoning in complex theories: The case of local theory extensions. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 47–71. Springer, Heidelberg (2007)
23. [TW68]
Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory 2(1), 57–81 (1968)
24. [Wei99]
Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC, pp. 129–136 (1999)Google Scholar
25. [WPK09]
Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Frontiers in Combining Systems (2009)Google Scholar
26. [YPK10]
Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 380–395. Springer, Heidelberg (2010)

## Copyright information

© Springer-Verlag Berlin Heidelberg 2010

## Authors and Affiliations

• Viktor Kuncak
• 1
• Ruzica Piskac
• 1
• Philippe Suter
• 1
1. 1.Swiss Federal Institute of Technology Lausanne (EPFL)

## Personalised recommendations

### Citepaper
{"ft_lang_label":"__label__en","ft_lang_prob":0.60320646,"math_prob":0.78291446,"size":7666,"snap":"2019-35-2019-39","text_gpt3_token_len":2170,"char_repetition_ratio":0.12816498,"word_repetition_ratio":0.028182702,"special_character_ratio":0.2731542,"punctuation_ratio":0.27009645,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.95879674,"pos_list":[0,1,2],"im_url_duplicate_count":[null,1,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-08-23T07:15:18Z\",\"WARC-Record-ID\":\"<urn:uuid:bd4d94f8-b6db-4ca7-bc44-e68ea06000cc>\",\"Content-Length\":\"91741\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:9b105b9d-3fbb-42f8-9914-9f16b0834274>\",\"WARC-Concurrent-To\":\"<urn:uuid:f12b1d61-cfde-4391-9b88-e910d95aba01>\",\"WARC-IP-Address\":\"151.101.248.95\",\"WARC-Target-URI\":\"https://link.springer.com/chapter/10.1007%2F978-3-642-15205-4_5\",\"WARC-Payload-Digest\":\"sha1:5KEPOYVVB26GNP4BUXOASMV4PAPPLE62\",\"WARC-Block-Digest\":\"sha1:DEKX42JXOUPYDCWPXFZCAVZFH3WSBYZS\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-35/CC-MAIN-2019-35_segments_1566027318011.89_warc_CC-MAIN-20190823062005-20190823084005-00118.warc.gz\"}"}