Non-Deterministic Database Transformation
Jump to navigation
Jump to search
A Non-Deterministic Database Transformation is database transformation task that ...
- Example(s):
- See: Database Query Task, Database Design Task, Database System, Relational Database, Transactional Database.
References
2016
- (Wang et al., 2016) ⇒ Wang, Q., Ferrarotti, F., Schewe, K. D., & Tec, L. (2016). A complete logic for non-deterministic database transformations. arXiv preprint arXiv:1602.07486
- Abstract: Database transformations provide a unifying framework for database 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 StateMachines (DB-ASMs). In this article we present a logic for DB-ASMs, extending the logic of Nanchen and St\"ark 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 {\Delta} generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.