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

Leave a comment