-
Views
-
Cite
Cite
Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec, Qing Wang, A complete logic for Database Abstract State Machines, Logic Journal of the IGPL, Volume 25, Issue 5, October 2017, Pages 700–740, https://doi.org/10.1093/jigpal/jzx021
Close - Share Icon Share
Abstract
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 formalization 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
