Checking SQL assertions

1 . A method for a Relational Database Management System, RDMS, to compile an SQL assertion into a set of SQL statements or views configured to check, at run-time, post-update satisfaction of the SQL assertion which means satisfaction of the SQL assertion after execution of an SQL update;

the RDMS comprising SQL assertions including the SQL assertion to be checked and relational tables having a consistent pre-update state, which means that the SQL assertions are satisfied before execution of the SQL update;

the SQL update and the SQL assertion to be checked affect or refer to one or more of the relational tables having a pre-update content which means content before execution of the SQL update; the method comprising:

creating, by execution of a CREATE TRIGGER statement, one or more SQL database triggers configured to simulate, at run-time, execution of the SQL update by providing one or more prospective relational tables, which are distinct from the affected relational tables, with a differential or modified content to be caused by execution of the SQL update, while keeping unaltered the pre-update content of the affected relational tables;

converting the SQL assertion to be checked into SQL statements or views configured to determine, at run-time, satisfaction or dissatisfaction of the SQL assertion depending on the pre-update content of the affected relational tables and the differential or modified content of the prospective relational tables; and

creating a procedure configured to commit or abort, at an end of a transaction responding to the SQL update, execution of the SQL update onto the affected relational tables depending on whether the SQL assertion to be checked has been determined satisfied or dissatisfied, respectively.

2 . A method according to claim 1 , the converting the SQL assertion to be checked into SQL statements or views comprising:

translating the SQL assertion to be checked into logics considering the affected relational tables;

modifying the logics to further consider the prospective relational tables; and

translating the modified logics back to SQL to generate the SQL statements or views.

3 . A method according to claim 2 , the translating the SQL assertion to be checked into logics and translating the logics back to SQL are based on Codd's theorem.

4 . A method according to claim 2 , the translating the SQL assertion to be checked into logics comprising translating the SQL assertion into logical rules including logic denials defining when the SQL assertion is violated, each of the logic denials having following form:

⊥← L 1 ∧ . . . ∧L n ∧B;

L i=1 . . . n being ordinary literals defining data existence or inexistence in affected tables, and B is a built-in literal defining selection of said existent or inexistent data causing violation of the SQL assertion.

5 . A method according to claim 4 , each of the ordinary literals L i=1 . . . n being a basic literal or an aggregate literal or a derived literal; and

the translating the SQL assertion into logical rules including, in case of derived literal, producing at least one derivation rule defining calculation of the derived literal and, in case of aggregate literal, producing at least one aggregation rule defining calculation of the aggregate literal.

6 . A method according to claim 5 , the translating SQL assertion into logical rules including applying an unfolding technique to minimize number of derivation rules.

7 . A method according to claim 5 , the translating SQL assertion into logical rules including translating derived literal and derivation rule or rules defining calculation thereof into aggregate literal and aggregation rule or rules defining calculation thereof.

8 . A method according to claim 5 , the modifying the logics to further consider the prospective relational tables including applying a disjunctive normal form transformation so that said modifying of the logics does not produce any logical rule with OR operator.

9 . A method according to claim 5 , the modifying the logics to further consider the prospective relational tables including applying following formula to each logic denial:

⊥←∧ i=1 . . . j−1 (old( L i )∧new( L j )∧∧ i=j+1 . . . n (old( L i )∨new( L i ))∧ B;

the function old(L) defining that L is true in the pre-update content and remains true with the differential or modified content, and function new(L) represents that the differential or modified content causes L to be true.

10 . A method according to claim 9 , the functions new(L) and old(L) being defined as follows when L is a basic literal:

new(L)=new(T)=ins_T, defining that existence of data T, expressed as T, is new if data T is within differential content as to be inserted by the SQL update;

new(L)=new(¬T)=del_T, defining that inexistence of data T, expressed as ¬T, is new if data T is within differential content as to be deleted by the SQL update;

old(L)=old(T)=T∧¬del_T, defining that existence of data T, expressed as T, is old if data T is within pre-update content and is not within differential content as to be deleted by the SQL update;

old(L)=old(¬T)=¬T∧¬ins_T, defining that inexistence of data T, expressed as ¬T, is old if data T is not within pre-update content and is not within differential content as to be inserted by the SQL update.

11 . A method according to claim 9 , the functions new(L) and old(L) being defined as follows when L is an aggregate literal:

new( T ( x,y )∧ w ( y,z ))=ins_ T ( x,y 1)∧del_ T ( x,y 2)∧ T ( x,y 3)∧ w ( y 3, z )∧ w ′( y 1, y 2)∧ w ( y 3+ y 1− y 2, z )

old( T ( x,y )∧ w ( y,z ))=ins_ T ( x,y 1)∧del_ T ( x,y 2)∧ T ( x,y 3)∧ w ( y 3, z )∧ w ( y 3+ y 1− y 2, z );

L referring to data T(x, y) in which x is a set of GROUP BY columns and y is aggregate value corresponding to said set of GROUP BY columns; and

w(y, z) is a condition referred to data T(x, y) and transformable into w′(y1, y2) and into w (y3, z) according to following table:

w(y, z)

w′(y1, y2)

w (y3, z)

y < z

y1 < y2

y3 >= z

y <= z

y1 < y2

y3 > z

y = z

y1 <> y2

y <> z

y >= z

y1 > y2

y < z

y > z

y1 > y2

y <= z

y <> z

y1 <> y2

y = z.

12 . A method according to claim 5 , the producing at least one aggregation rule defining calculation of the aggregate literal including:

producing one or more insertion aggregation rules defining calculation part of the aggregate literal due to data included in differential content as to be inserted by the SQL update;

producing one or more deletion aggregation rules defining calculation part of the aggregate literal due to data included in differential content as to be deleted by the SQL update.

13 . A method according to claim 12 , the aggregation rule has following form:

p ( x ,ƒ ( y ))← L 1 ∧ . . . ∧L n ∧B;

and producing one or more insertion aggregation rules including applying following formula to said aggregation rule:

ins_ p j ( x ,ƒ( y ))←∧ i=1 . . . j−1 (old( L i ))∧new( L j )∧∧ i=j+1 . . . n (old( L i )∨new( L i ))∧ B.

14 . A method according to claim 12 , the aggregation rule has following form:

p ( x ,ƒ ( y ))← L 1 ∧ . . . ∧L n ∧B;

and the producing one or more deletion aggregation rules including applying following formula to said aggregation rule:

del_ p j ( x ,ƒ ( y ))←∧ i=1 . . . j−1 (old( L i ))∧new(¬ L j )∧∧ i=j+1 . . . n ( L i )∧ B.

15 . A system for a Relational Database Management System, RDMS, to compile an SQL assertion into a set of SQL statements or views configured to check, at run-time, post-update satisfaction of the SQL assertion which means satisfaction of the SQL assertion after execution of an SQL update;

the RDMS SQL assertions including the SQL assertion to be checked and relational tables having a consistent pre-update state, which means that the SQL assertions are satisfied before execution of the SQL update;

the SQL update and the SQL assertion to be checked affect or refer to one or more of the relational tables having a pre-update content which means content before execution of the SQL update; the system comprising:

a processor, and

a memory storing executable instructions that, when executed by the processor, cause the system to perform a method of:

creating, by execution of a CREATE TRIGGER statement, one or more SQL database triggers configured to simulate, at run-time, execution of the SQL update by providing one or more prospective relational tables, which are distinct from the affected relational tables, with a differential or modified content to be caused by execution of the SQL update, while keeping unaltered the pre-update content of the affected relational tables;

converting the SQL assertion to be checked into SQL statements or views configured to determine, at run-time, satisfaction or dissatisfaction of the SQL assertion depending on the pre-update content of the affected relational tables and the differential or modified content of the prospective relational tables; and

creating a procedure configured to commit or abort, at an end of a transaction corresponding to the SQL update, execution of the SQL update onto the affected relational tables depending on whether the SQL assertion to be checked has been determined satisfied or dissatisfied, respectively.