Traduction mécanisée et certifiée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée ; A Coq certified translation from an extension of relational algebra for SQL to a nested algebra
Titel:
Traduction mécanisée et certifiée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée ; A Coq certified translation from an extension of relational algebra for SQL to a nested algebra
Beteiligte:
Hachmaoui, Mohammed Houssem Eddine
[VerfasserIn]
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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 multiensemble 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 NRAᵉ, 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. ; In 1974, Boyce and Chamberlin created sql using the concepts of the relational algebra proposed by Codd in 1970, but as it evolved, its formal semantics became more and more complex. The small fragment select from where of SQL can be mapped to a relational algebra, with bag's semantics and by restricting expressions and formulae to those which can be expressed in relational algebra. To ...