Specification of Database Evolution in Active Databases - Formulating Correctness of Triggers

Many database systems and the SQL3 database standard have active features that allow specification of static constraints -- NOT NULL constraints, Column defaults, Unique indexes, Check constraints, Primary key constraints, and Foreign key constraints, and triggers. Intuitively, triggers are supposed to capture the desired semantic behavior of the stored data and its evolution. But, not much attention towards formally specifying this -- especially the dynamic aspects -- has been paid. In this paper we show how the `desired semantic behavior' can be specified in a logical language with temporal and aggregate operators. We refer to this specification as the evolution specification of an active database and formulate the correctness of triggers with respect to a given evolution specification. We show that without the evolution specification, no or very weak formal claims can be made about the correctness of triggers. We also discuss how to obtain triggers from the evolution specification. ..