Can some developer kindly post a link to related published research?

[practicum]

I am very intrigued by this github project. I am working on related ideas involving assertion-checking and SQL code for my Master's thesis.

Have there been any published papers I could reference regarding this 'yszheda/assertion-verification' project?

Are there any planned papers in the works?

Thanks! Congratulations on a very interesting project.

[yszheda]

Dear practicum,
Thank you for your interest in the project!

As for the reference papers, I think you can have a look at "Static management of integrity in object-oriented databases: Design and implementation" on EDBT'98:
http://link.springer.com/chapter/10.1007%2FBFb0100993
This paper clearly explains how to achieve compile-time violation prevention in database integrity constraint checking.
(BTW. One of its authors is one of my former supervisors. XD)

Actually, this project is my work for bachelor thesis. I did do surveys and write a thesis paper, but it was mainly in Chinese. If you are still interested to read more related papers, maybe you can leave me your email and I send the bibtex file to you. XD

As I mentioned above, this project is just a piece of bachelor work. It is still too naive and incomplete in research to get published. For example, the widely used aggregate functions are not supported. In my survey, the problem of verifying constraints containing aggregate functions is so challenging that only a few papers have handled it. If you can present some approach and implement it in your work, that would be wonderful! Good luck!

[practicum]

Dear yszheda,

Thank you very much for the link to the EDBT'98 article. I will check it out.

My work has been influenced by a Microsoft paper about a tool named 'Qex'. Qex uses first order theories to represent SQL queries, and then the theories are fed to an SMT solver together with some assertion or constraint in order to check whether the whole formula is satisfiable.

Notably, Qex indeed does support aggregate functions!

Details available here:

http://research.microsoft.com/apps/pubs/default.aspx?id=131320
http://research.microsoft.com/en-us/projects/qex/

I will give you my email address offline (off-github), and if you could send me your Bibtex file I would love that.

Kind regards!

[yszheda]

Thank you very much for sharing, practicum!

It sounds promising that Qex have already support aggregate functions without using higher order logic. I would like to check whether Qex solve the problem of detecting violation from database updates on the basis of assertions, which is the goal of the 'assertion-verification' project. And I am curious to figure out how it handle aggregate functions.

[zhangysh1995]

detecting violation from database updates on the basis of assertions

A bit too late, but could you explain this sentence? Do you mean database updates will result in violations?

[practicum]

Hi @zhangysh1995,

Since you are quoting @yszheda directly, I suppose only @yszheda can give the true answer about what was meant by detecting violations from database updates.

However, since it was relevant in my thesis:

Satisfiability checking for quality assurance in relational data processing
California State University, Long Beach, 2013
https://pqdtopen.proquest.com/doc/1449155537.html?FMT=ABS

... it seems potentially helpful for me to state how I interpret that phrase.

(The thesis is available free online. Refer to Chapter 2 for complete examples of proposed database assertions.)

I was concerned not with the kinds of UPDATE statements that act on individual rows.

Rather, I was concerned with DDL statements that update the schema, and how to provide better checking that those DDL schema changes are safe for a given codebase.

When you use DDL to alter table definitions, most tooling can help catch "obvious" syntax issues, such as how a column rename will render invalid any SELECT statement that uses an obsolete column name.

However, there are other ways to alter tables that cause problems that are harder to spot.

For example, altering a table column to make it nullable can have a dangerous impact on existing SQL code in a codebase. It can subtly change the semantics and behavior of existing SQL queries (dangerously so because it might take a while for issues to become apparent, and it might seem intermittent, because it depends on whether any new NULL cells flow throw the query or not).

[zhangysh1995]

I quickly skimmed a part of Chapter 2. If I understand correctly, the aim of the thesis is verifying the correctness of SQL queries. For example, the NULL could cause unexpected problems by an inappropriate update on the table schema.

Following the example in Fig. 5 (page 17), how could we define the initial query behavior wanted by the developer?

The code is only correct as long as each customer initiates no more than one claim per day

Could this be the original specification of the table schema? Then, how could we differentiate the real bugs from the unintended defects?

Because I haven't finished reading the full thesis, those questions could be arguably very obvious.

I'm reading papers regarding quality assurance in DBMSs, and your thesis really inspired for another possibility. To be honest, I haven't thought about the bugs in SQL itself.

BTW, my English name is also Kelly, though it is a randomly chosen one ;)

[practicum]

Kellys, unite! :)

Following the example in Fig. 5 (page 17), how could we define the initial query behavior wanted by the developer?

• "The code is only correct as long as each customer initiates no more than one claim per day"

Could this be the original specification of the table schema? Then, how could we differentiate the real bugs from the unintended defects?

Wow! These questions are exactly what I would hope someone would ask. This is exactly the kind of thinking that I myself became obsessed with during my project.

I am going to write my reply right now without looking back at my Chapter 2. My reply should be self-contained and make sense on its own. However, since I have not reread Chapter 2, the words that I type today might appear "slightly off topic." So try to just take my current reply as a separate entity and don't be too bothered if you can't find obvious support for it in Chapter 2. (But feel free to ask more questions, about both Chapter 2 and today's discussion.)

"one claim per day" <--- "could this be the original specification of the table schema?"

Yes, it would be possible to add constraints (such as CHECK constraints) to the table definition to enforce such a rule. Anyone trying to insert more than one claim per day would find that their INSERT attempt would get an error.

how could we differentiate the real bugs from the unintended defects?

My proposed (partial?) solution: a new kind of "assertion" that becomes part of the SELECT query itself.

This problem of differentiating a coding bug from a platform defect... this is a "universal" problem that I think extends beyond SQL and RDBMS. And from what I have seen, the "universal" answer is: assertions/preconditions/postconditions (aka "formal specification")

You could ask an even more basic question:

"How could we differentiate whether this 'weird' output of a SQL query is a bug or whether the query author wanted this 'weird' output?"

Assume the author of the query is not available to explain their intent.

You could:

1. take the literal SQL "as gospel" (aka "as the perfect word of god") and say that the author definitely wanted this output, because this is exactly the query that was written. ... or...
2. you could apply your own experience and judgement and critical thinking and deem for yourself that the SQL query was improperly coded and should be fixed

If the original SQL author had also written formal preconditions and postconditions, then you would have much better evidence to choose between (1) and (2).

And here is where we circle back to consider how the CHECK constraint option enters this discussion in a "dangerous" way.

Imagine that (1) was originally correct. Maybe the author of the SQL query wrote a perfect, correct SQL query given the table schema of that point in time. Maybe the query was correct given the guarantee offered by a CHECK constraint that was part of the system at that time.

Oh no....

• Removing the CHECK constraint turns an originally perfectly written SQL query into a "buggy" SQL query!

And nothing changed about the query!

Most (all?) DBMS systems have no way to prevent this or even warn about it. Anyone who wants to alter a table definition would need to find every query that relies on that table and then simply "try to imagine" whether the table change will break that SQL query or not. (Sidenote: if any DBMS developers can post links to systems that do prevent or warn in this situation, that would be excellent news!)

If the SQL query itself could carry with it a precondition statement such as:

• (To run this query), it MUST be true that for all date-customer pairs in the Claim table, at most one Claim per date-customer pair exists.

If this precondition were machine-checkable against the table schema, then we could achieve automatic error detection for someone attempting to delete a CHECK constraint from a table, and automated links to the queries that rely on that CHECK.

[zhangysh1995]

You could:

take the literal SQL "as gospel" (aka "as the perfect word of god") and say that the author definitely wanted this output, because this is exactly the query that was written. ... or...
you could apply your own experience and judgement and critical thinking and deem for yourself that the SQL query was improperly coded and should be fixed

I would say the first way is more scientific. Based on the "perfectness" assumption, it would be possible to check inconsistency in the database. I couldn't give a concrete example here, but it gives me an idea for automating the checking process.

Most (all?) DBMS systems have no way to prevent this or even warn about it. Anyone who wants to alter a table definition would need to find every query that relies on that table and then simply "try to imagine" whether the table change will break that SQL query or not. (Sidenote: if any DBMS developers can post links to systems that do prevent or warn in this situation, that would be excellent news!)

I suppose what you describe here is an interactive debugging utility which gives the user a tip if the operation will raise an error(?). I have some similar thoughts but I didn't know where to start. It seems checking constraints could be a good starting point.

If the SQL query itself could carry with it a precondition statement such as:

(To run this query), it MUST be true that for all date-customer pairs in the Claim table, at most one Claim per date-customer pair exists.

I think this is very similar to dependency extraction from the queries? We extract the requirement that "at most one Claim per date-customer pair exists" from the query.

If this precondition were machine-checkable against the table schema, then we could achieve automatic error detection for someone attempting to delete a CHECK constraint from a table, and automated links to the queries that rely on that CHECK.

This would be a good idea from my point of view! The first step towards the automation should be understanding the queries and form a linkage among them (constraints, dependencies...). This process will fall into the scope of static analysis.

Fortunately, I'm looking for research project in this direction. I think I will find related works and see if I could start to work on it. If you're also interested, we could cooperate on it!

I don't think here in the issue is a good place for detailed discussions. Maybe we should continue the conversations in the email. Because I don't see your email address in the profile, could you please send me an email and say hello? If you're more comfortable with GitHub, we could still discuss here ;)

SQL Server has a similar functionality to show dependencies, here.