SQL query evaluation with correctness guarantees

Pq SQL ? :

• $25B/year
• grosse communauté de data scientists

Réponses certaines :

“Correctness guarantee” : $Eval(Q,D)\subseteq cer{t}_{\mathrm{\perp }}(Q,D)$

On remplace les “Non Ou” par des “Et Non” (à la “De Morgan”)

Pour démontrer les théorèmes précédents, on pose une “sémantique” à SQL (arbitraire).

Préservation par homomorphisme “strong onto” inverse

Base de donnée incomplète : il y manque des données

Ex :

• Champ optionnels
• Héritage basique
• …

Propriété régulières des arbres (en logique épistémique dynamique)

#

Logique de Hoare