Abstract
This paper explores formal verification in the area of database technology, in particular how to reason about queries and updates in a database system. The formalism is sufficiently general to be applicable to relational and graph databases. We first define a domain-specific language consisting of nested query and update primitives, and give its operational semantics. Queries are in full first-order logic. The problem we try to solve is whether a database satisfying a given pre-condition will satisfy a given post-condition after execution of a given sequence of queries and updates. We propose a weakest-precondition calculus and prove its correctness. We finally examine a restriction of our framework that produces formulas in the guarded fragment of predicate logic and thus leads to a decidable proof problem.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Parts of the development can be found in the repository https://bitbucket.org/Martin_Strecker/db_queries_updates/.
- 2.
We use the same relation symbol \(\,\models \,\) and disambiguate individual and set-based semantics with the designation of the model (\(\iota \) resp. \(\sigma \)).
References
Ahmetaj, S., Calvanese, D., Ortiz, M., Simkus, M.: Managing change in graph-structured data using description logics. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI 2014), pp. 966–973. AAAI Press (2014). http://www.inf.unibz.it/~calvanese/papers-html/AAAI-2014-graph-dbs.html
Ahmetaj, S., Calvanese, D., Ortiz, M., Simkus, M.: Managing change in graph-structured data using description logics. ACM Trans. Comput. Log. 18(4), 27:1–27:35 (2017). https://doi.org/10.1145/3143803
Ahmeti, A., Calvanese, D., Polleres, A.: Updating RDFS ABoxes and TBoxes in SPARQL. In: Mika, P., et al. (eds.) ISWC 2014. LNCS, vol. 8796, pp. 441–456. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11964-9_28
Andréka, H., Németi, I., van Benthem, J.: Modal languages and bounded fragments of predicate logic. J. Philos. Log. 27(3), 217–274 (1998). http://www.fenrong.net/teaching/Andreka.pdf
Benedikt, M., Griffin, T., Libkin, L.: Verifiable properties of database transactions. Inf. Comput. 147(1), 57–88 (1998). https://core.ac.uk/download/pdf/82337092.pdf
Brenas, J.H., Echahed, R., Strecker, M.: Ensuring correctness of model transformations while remaining decidable. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 315–332. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_18
Brenas, J.H., Echahed, R., Strecker, M.: A Hoare-like calculus using the SROIQ\(^{\sigma }\) logic on transformations of graphs. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 164–178. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44602-7_14
Bry, F., Decker, H., Manthey, R.: A uniform approach to constraint satisfaction and constraint satisfiability in deductive databases. In: Schmidt, J.W., Ceri, S., Missikoff, M. (eds.) EDBT 1988. LNCS, vol. 303, pp. 488–505. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-19074-0_69
Chaabani, M., Echahed, R., Strecker, M.: Logical foundations for reasoning about transformations of knowledge bases. In: Eiter, T., Glimm, B., Kazakov, Y., Krötzsch, M. (eds.) DL - Description Logics. CEUR Workshop Proceedings, vol. 1014, pp. 616–627. CEUR-WS.org (2013)
Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic, a Language Theoretic Approach. Cambridge University Press (2011). http://www.labri.fr/perso/courcell/Book/TheBook.pdf
Fagin, R., Ullman, J.D., Vardi, M.Y.: On the semantics of updates in databases. In: Proceedings of the 2nd ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, pp. 352–365. ACM (1983)
Francis, N., et al.: Cypher: An evolving query language for property graphs. In: Proceedings of the 2018 International Conference on Management of Data, SIGMOD Conference 2018, Houston, TX, USA, 10–15 June 2018, pp. 1433–1445 (2018). https://doi.org/10.1145/3183713.3190657. https://doi.org/10.1145/3183713.3190657
Grädel, E.: Decision procedures for guarded logics. In: Ganzinger, H. (ed.) CADE 1999. LNCS, vol. 1632, pp. 31–51. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48660-7_3
Grädel, E.: On the restraining power of guards. J. Symb. Log. 64, 1719–1742 (1999). http://www.logic.rwth-aachen.de/pub/graedel/Gr-jsl99.ps
Grädel, E.: Decidable fragments of first-order and fixed-point logic. From prefix-vocabulary classes to guarded logics. In: Proceedings of Kalmár Workshop on Logic and Computer Science, Szeged (2003). http://www.logic.rwth-aachen.de/pub/graedel/Gr-kalmar03.ps
Habel, A., Pennemann, K.-H., Rensink, A.: Weakest preconditions for high-level programs. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 445–460. Springer, Heidelberg (2006). https://doi.org/10.1007/11841883_31
Hirsch, C.: Guarded logics: algorithms and bisimulation. Ph.D. thesis, RWTH Aachen (2002). http://www.logic.rwth-aachen.de/pub/hirsch/hirsch.pdf
Hladik, J.: Implementation and optimisation of a tableau algorithm for the guarded fragment. In: Egly, U., Fermüller, C.G. (eds.) TABLEAUX 2002. LNCS, vol. 2381, pp. 145–159. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45616-3_11
Hosoya, H.: XML Processing - The Tree-Automata Approach. Cambridge University Press, Cambridge (2011)
Inaba, K., Hidaka, S., Hu, Z., Kato, H., Nakano, K.: Graph-transformation verification using monadic second-order logic. In: International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 17–28, July 2011. http://dl.acm.org/authorize?442117
Itzhaky, S., et al.: On the automated verification of web applications with embedded SQL. In: Benedikt, M., Orsi, G. (eds.) 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 68, pp. 16:1–16:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2017). https://doi.org/10.4230/LIPIcs.ICDT.2017.16. http://drops.dagstuhl.de/opus/volltexte/2017/7050
Martens, W., Neven, F.: Frontiers of tractability for typechecking simple XML transformations. J. Comput. Syst. Sci. 73(3), 362–390 (2007)
Martinenghi, D., Christiansen, H., Decker, H.: Integrity checking and maintenance in relational and deductive database and beyond. In: Intelligent Databases: Technologies and Applications, pp. 238–285. IGI Global (2007)
Muchnick, S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, Burlington (1997)
Nipkow, T., Klein, G.: Concrete Semantics (2014). http://concrete-semantics.org/
Olivé, A.: Integrity constraints checking in deductive databases. In: VLDB, pp. 513–523. Citeseer (1991)
openCypher Project: Cypher Query Language Reference, version 9 edn. (2018). http://www.opencypher.org/
Acknowledgements
We are grateful to Lison Kardassevitch for implementing a prototype of the verification framework.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Brenas, J.H., Echahed, R., Strecker, M. (2019). Reasoning Formally About Database Queries and Updates. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_33
Download citation
DOI: https://doi.org/10.1007/978-3-030-30942-8_33
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30941-1
Online ISBN: 978-3-030-30942-8
eBook Packages: Computer ScienceComputer Science (R0)