Advertisement

Reasoning Formally About Database Queries and Updates

  • Jon Haël Brenas
  • Rachid Echahed
  • Martin Strecker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

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.

Keywords

Automated theorem proving Modal logic Graph transformations Program verification 

Notes

Acknowledgements

We are grateful to Lison Kardassevitch for implementing a prototype of the verification framework.

References

  1. 1.
    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
  2. 2.
    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/3143803MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    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_28CrossRefGoogle Scholar
  4. 4.
    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.pdfMathSciNetCrossRefGoogle Scholar
  5. 5.
    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.pdfMathSciNetCrossRefGoogle Scholar
  6. 6.
    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_18CrossRefzbMATHGoogle Scholar
  7. 7.
    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_14CrossRefGoogle Scholar
  8. 8.
    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_69CrossRefGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    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
  11. 11.
    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)Google Scholar
  12. 12.
    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
  13. 13.
    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_3CrossRefGoogle Scholar
  14. 14.
    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.psMathSciNetCrossRefGoogle Scholar
  15. 15.
    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
  16. 16.
    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_31CrossRefGoogle Scholar
  17. 17.
    Hirsch, C.: Guarded logics: algorithms and bisimulation. Ph.D. thesis, RWTH Aachen (2002). http://www.logic.rwth-aachen.de/pub/hirsch/hirsch.pdf
  18. 18.
    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_11CrossRefGoogle Scholar
  19. 19.
    Hosoya, H.: XML Processing - The Tree-Automata Approach. Cambridge University Press, Cambridge (2011)zbMATHGoogle Scholar
  20. 20.
    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
  21. 21.
    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
  22. 22.
    Martens, W., Neven, F.: Frontiers of tractability for typechecking simple XML transformations. J. Comput. Syst. Sci. 73(3), 362–390 (2007)MathSciNetCrossRefGoogle Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    Muchnick, S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, Burlington (1997)Google Scholar
  25. 25.
    Nipkow, T., Klein, G.: Concrete Semantics (2014). http://concrete-semantics.org/
  26. 26.
    Olivé, A.: Integrity constraints checking in deductive databases. In: VLDB, pp. 513–523. Citeseer (1991)Google Scholar
  27. 27.
    openCypher Project: Cypher Query Language Reference, version 9 edn. (2018). http://www.opencypher.org/

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.UTHSC - ORNLMemphisUSA
  2. 2.CNRS and University Grenoble AlpesGrenobleFrance
  3. 3.ToulouseFrance

Personalised recommendations