Proving an Upgrade is Possible

Let's define some terms.

First, the state of the database before the upgrade is S(1). The state after the upgrade will be S(2). The operation we wish to pre-validate is S(1)->S(2). Let's get back to this after looking at other stuff.

But before we validate the state change, we should validate that the proposed new meta-State will be valid. The database's meta-State is described in normalized tables (real 1NF, no lists please). The meta-State before the upgrade is mS(1), which we assume to be valid. We must validate the proposed new meta-State, mS(2). But this easy because it is in normalized tables, and we can use integrity and referential constraints to ensure it is valid.

So having validated our destination mS(2), we should also now determine that the change in meta-State is valid. This would be to prevent things like converting a column from char to int (or perhaps defining what should happen if one were to do that). Since mS(1) is a set of tables, and mS(2) is a set of the same structure tables, the operation mS(1)->mS(2) can be described in a third set of tables, delta-meta-State, or dmS. We obtain this set of tables by outer joining all corresponding tables in mS(1) and mS(2). We can then have a fourth set of tables that can be used to do referential checks on dmS and determine if it is valid.

The point that is bugging me is that, if we can prove mS(2) is valid, and that dmS is valid, does that imply that dS ( S(1)->S(2) ) is valid? Can it be proven to be valid without producing database S(2) and then database dS, because such a task is insane in actual practice.

So I guess I am looking for a theorem that says, "Given S(1), S(2) and mS(1) and mS(2), where S(1) mS(1), ms(2) and dmS are all known to be valid, it can be safely concluded that dS and S(2) will be valid". Wondering if anybody has seen a rigorous mathematical treatment of this subject, and what the Google terms might be.

-- 
Kenneth Downs
Secure Data Software, Inc.
(Ken)nneth_at_(Sec)ure(Dat)a(.com)