Thèse en cours
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Traduction certifiée et mécanisée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée
Début le 01/10/2016
Direction : CONTEJEAN, Evelyne
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI - VLAS
Soutenue le 16/11/2020 devant le jury composé de :
- Nicolas Thiéry Professeur, Université Paris Saclay Examinateur
- Alan Schmitt Directeur de recherche, Inria Rennes Rapporteur et examinateur
- Mohan-Saïd Hacid Professeur, Université Claude Bernard Lyon 1 (LIRIS) Rapporteur
- Sophie Tison Professeure, Université Lille 1 Examinatrice
- Nicolas Tabareau Directeur de recherche, Inria Nantes Examinateur
- Évelyne Contejean Directrice de recherche, CNRS - Université Paris-Saclay Directrice
- Véronique Benzaken Professeure, Université Paris-Saclay Directrice
- Chantal Keller Maître de Conférences, Université Paris-Saclay Directrice
Activités de recherche :
Résumé :
Résumé: En 1974, Boyce et Chamberlin ont créé le langage SQL en se basant sur l’algèbre relationnelle
proposée par Codd en 1970, mais à mesure d’extensions, la sémantique formelle de SQL s’est éloignée de celle
de l’algèbre relationnelle. Le petit fragment select from where de SQL peut correspondre à une algèbre relationnelle
avec une sémantique multiensembliste en restreignant les expressions et les formules à celles exprimables en algèbre
relationnelle. Pour capturer la sémantique du fragment beaucoup plus réaliste select from where group by having
en prenant en compte toutes les expressions y compris celles avec agrégats, toutes les formes de formules,
les valeurs nulles et, encore plus subtil, les environnements très particuliers de SQL, Benzaken et Contejean ont proposé
l’algèbre SQLAlg qui est une extension de l’algèbre relationnelle avec un nouvel opérateur pour la partie group by having conçu
spécifiquement pour prendre en compte tous les aspects de SQL cités précédemment.
Ce même fragment de SQL, avec toute ses subtilités, est-il capturable par l’algèbre relationnelle imbriquée ? Cette thèse prouve formellement
que oui. En effet, nous proposons une traduction, certifiée en Coq, de SQLAlg vers NRAe , qui est une formalisation en Coq de l’algèbre relationnelle imbriquée.
La traduction prend en compte les expressions simples et complexes, les formules SQL et reflète parfaitement comment les environnements sont
construits et manipulés, spécialement pour les agrégats et les requêtes corrélées. Ce travail s’inscrit dans un cadre plus global, celui du
projet DBCert : une chaîne de compilation certifiée en Coq de SQL vers JavaScript.
