Abstract
In this paper we present a decision procedure for Restricted Intensional Sets (RIS), i.e. sets given by a property rather than by enumerating their elements, similar to set comprehensions available in specification languages such as B and Z. The proposed procedure is parametric with respect to a first-order language and theory \(\mathcal {X}\), providing at least equality and a decision procedure to check for satisfiability of \(\mathcal {X}\)-formulas. We show how this framework can be applied when \(\mathcal {X}\) is the theory of hereditarily finite sets as is supported by the language CLP(\(\mathcal {SET}\)). We also present a working implementation of RIS as part of the \(\{log\}\) tool and we show how it compares with a mainstream solver and how it helps in the automatic verification of code fragments.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The form of RIS terms is borrowed from the form of set comprehension expressions available in Z.
- 2.
This is guaranteed by procedure remove_neq (see Sect. 3).
- 3.
More precisely, each solution of \(\varPhi \) expanded to the variables occurring in \(\phi _i\) but not in \(\varPhi \), so to account for the possible fresh variables introduced into \(\phi _i\).
References
Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_8
Cantone, D., Longo, C.: A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions. Theor. Comput. Sci. 560, 307–325 (2014). http://dx.doi.org/10.1016/j.tcs.2014.03.021
Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model building. In: CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, pp. 11–27 (2003)
Cristiá, M., Rossi, G.: Restricted insentional sets. http://people.dmi.unipr.it/gianfranco.rossi/SETLOG/risCADEonline.pdf
Cristiá, M., Rossi, G.: A decision procedure for sets, binary relations and partial functions. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part I. LNCS, vol. 9779, pp. 179–198. Springer, Cham (2016). doi:10.1007/978-3-319-41528-4_10
Dal Palú, A., Dovier, A., Pontelli, E., Rossi, G.: Integrating finite domain constraints and CLP with sets. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, PPDP 2003, pp. 219–229. ACM, New York (2003). http://doi.acm.org/10.1145/888251.888272
Deharbe, D., Fontaine, P., Paleo, B.W.: Quantifier inference rules for SMT proofs. In: Workshop on Proof eXchange for Theorem Proving (2011)
Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: A language for programming in logic with finite sets. J. Log. Program. 28(1), 1–44 (1996). http://dx.doi.org/10.1016/0743-1066(95)00147-6
Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000)
Dovier, A., Pontelli, E., Rossi, G.: Intensional sets in CLP. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 284–299. Springer, Heidelberg (2003). doi:10.1007/978-3-540-24599-5_20
Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theor. Pract. Log. Program. 6(6), 645–701 (2006). http://dx.doi.org/10.1017/S1471068406002730
Drăgoi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 161–181. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54013-4_10
Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_25
Hill, P.M., Lloyd, J.W.: The Gödel Programming Language. MIT Press, Cambridge (1994)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45236-2_46
Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_38
Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_42
Rossi, G.: \(\{log\}\) (2008). http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html
Schneider, S.: The B-method: An Introduction. Cornerstones of Computing. Palgrave (2001). http://books.google.com.ar/books?id=Krs0OQAACAAJ
Schwartz, J.T., Dewar, R.B.K., Dubinsky, E., Schonberg, E.: Programming with Sets - An Introduction to SETL. Texts and Monographs in Computer Science. Springer, New York (1986). http://dx.doi.org/10.1007/978-1-4613-9575-1
Veanes, M., Saabas, A.: On bounded reachability of programs with set comprehensions. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 305–317. Springer, Heidelberg (2008). doi:10.1007/978-3-540-89439-1_22
Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 366–382. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04222-5_23
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc., Upper Saddle River (1996)
Zhang, J., Zhang, H.: System description generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308–312. Springer, Heidelberg (1996). doi:10.1007/3-540-61511-3_96
Acknowledgements
Part of the work of M. Cristiá is supported by ANPCyT’s grant PICT-2014-2200.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Cristiá, M., Rossi, G. (2017). A Decision Procedure for Restricted Intensional Sets. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-63046-5_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63045-8
Online ISBN: 978-3-319-63046-5
eBook Packages: Computer ScienceComputer Science (R0)