Re: Proving an Upgrade is Possible

Jan Hidders wrote:

> Kenneth Downs wrote:

>> Jan Hidders wrote:
>>>Kenneth Downs wrote:
>>>>Jan Hidders wrote:
>>>>
>>>>>Ok, so I suspect are you asking the following:
>>>>>
>>>>>"Given the old database schema and a few updates to its constraints
>>>>>(but not its structure) is it possible to algorithmically decide (or
>>>>>mathematically prove) whether all instances of the old schema are also
>>>>>instances of the new schema?"
>>>>>
>>>>>I leave it to you whether it is "algorithmically decide" or
>>>>>"mathematically prove".
>>>>
>>>>You are on target, except that constraints are included, and also
>>>>automation
>>>>(columns like price_extended = price * qty).  So while we are at it,
>>>>this means things like NULL/NOT NULL rules, DEFAULT values and so forth.
>>>
>>>What do you mean by "constraints are included"? Those were already
>>>included in my formulation. Since you only care about whether instances
>>>are valid or not, automation can in this case be regarded as a special
>>>case of constraints. Default values are completely irrelevant for your
>>>question because they do not change the set of allowed valid instances.
>> 
>> To provide an analytic and deterministic answer to the viability of any
>> db change, you must consider constraints, null rules, and defaults.
>> 
>> Consider this case.  Add two columns to a table, COL_A and COL_B, with
>> the
>> constraint that COL_A < COL_B.  One has a default value, the other does
>> not, and they may not be null.  What on Earth  do you do to satisfy these
>> requirements in the rows that already exist in the table?

Exactly.

>
> To what extent these problems are solvable or not depends upon a lot of
> details such as if you consider each schema update as a sequence of
> atomic updates or as one big update, but also the nature of the
> constraints that are allowed or the type of queries that may be used for
> derived columns/tables. So until you give an idea of what your update
> language and its semantics are, how the constraint language looks what
> type of queries you allow for derived data it's hard to give a
> meaningful answer to your question.

Here is our current specification for database specifications:

http://www.secdat.com/dev/androspec.html

It is pretty thorough in terms of what it can define, but it is still lacking in the topic of this thread: fully and completely determining that an upgrade is possible. I usually start a thread on something here before tackling a problem.

>

>> upgrade will succeed.  I did not choose your term "algorithmically
>> decide" because it is not a step-by-step code thing, the validity or
>> invalidity of the state change should be captured in the state of the
>> meta-data. For the
>> same reason I did not choose your term "mathematically prove". 
>> Demonstrate by Analysis seems closer to the mark because we want to
>> examine (or analyze) the meta-data.

Methinks we are in fact saying the same thing. My final word on it would be that we cast the "mathematical proof" of the validity of the upgrade to the act of examining some meta-data tables for conventional stuff like unique and referential violations.

The question of infinite possibilities is tough. You don't have to resort to Godel to know that any set of features will be unsatisfactory for all possible cases, but you can at least prove that any operation involving those features is valid or not valid. If the primitive operations are powerful enough in combination, you can safely cast all problems in terms of those primitives.

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