A Complete Logic for Non-Deterministic Database Transformations
Sprache des Titels:
Englisch
Original Kurzfassung:
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 State Machines (DB-ASMs).
In this article we present a logic for DB-ASMs, extending the logic of Nanchen and Stark 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.
Forschungs-