A complete logic for Database Abstract State Machines. (6th July 2017)

• Record Type: Journal Article
• Authors: Ferrarotti, Flavio; Schewe, Klaus-Dieter; Tec, Loredana; Wang, Qing
• Is Part Of: Logic journal of the IGPL. Volume 25:Number 5(2017:Oct.)
• Page Start: 700
• Page End: 740
• Publication Date: 2017-07-06
• Subjects: Database transformation -- abstract state machine -- complete logic; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/jigpal/jzx021
• Languages: English
• ISSNs: 1367-0751

Abstract

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 $[X]$, where $X$ is interpreted as an update set $\Delta$ generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.