  In database theory, the term $\textit{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\"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.
