Reasoning Formally about Database Queries and Updates

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.
 

Online Copy

• Conference paper: (personal copy) (publisher's version)

BibTeX Entry

(preliminary)

@InProceedings{brenas19:_reason_formal_datab_queries_updat,
  author =    {Jon Haël Brenas and Rachid Echahed and Martin Strecker},
  title =     {Reasoning Formally about Database Queries and Updates},
  booktitle = {FM'2019},
  year =      2019,
  editor =    {Maurice ter Beek and Annabelle McIver and José Oliveira},
  series =    {LNCS},
  publisher = {Springer},
  url       = {http://martin-strecker.org/Publications/fm2019.html},
  note =      {to appear}
}