A complete logic for database abstract state machines

Authors Flavio Ferrarotti
Klaus-Dieter Schewe
Loredana Tec
Qing Wang
Title A complete logic for database abstract state machines
Type article
Journal Logic Journal of the IGPL
DOI 10.1093/jigpal/jzx021
Month July
Year 2017
Pages 700-740
SCCH ID# 17015

In database theory, the term database transformation was used to refer to a unifying treatment for computable queries and updates. Recently, it was shown that non-deterministic database transformations can be captured exactly by a variant of ASMs, the so-called Database Abstract State Machines (DB-ASMs). In this article we present a logic for DB-ASMs, extending the logic of Nanchen and Stärk for ASMs. In particular, we develop a rigorous proof system for the logic for DB-ASMs, which is proven to be sound and complete. The most difficult challenge to be handled by the extension is a proper formalisation capturing non-determinism of database transformations and all its related features such as consistency, update sets or multisets associated with DB-ASM rules. As the database part of a state of database transformations is a finite structure and DB-ASMs are restricted by allowing quantifiers only over the database part of a state, we resolve this problem by taking update sets explicitly into the logic, i.e. by using an additional modal operator [X], where X is interpreted as an update set ^ generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.