Conférences (Rapports L3) 6 Septembre

SQL query evaluation with correctness guarantees

Pq SQL ? :

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

Réponses certaines :

\[cert(Q,D) = \bigcap Q(v(D))\]

“Correctness guarantee” : \(Eval(Q,D) ⊆ cert_{\bot}(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