0HAL编号：tel-030268350https://theses.hal.science/tel-030268350提交日期：2020年11月26日0HAL是一个多学科开放存取档案，用于存储和传播科学研究文献，无论其是否发表。这些文献可以来自法国或国外的教育和研究机构，也可以来自公共或私人研究中心。0HAL多学科开放存取档案，旨在存储和传播法国或国外教育和研究机构、公共或私人实验室发表或未发表的研究级科学文献。0SQL扩展的机械化和Coq认证翻译到嵌套代数0Mohammed Houssem Eddine Hachmaoui0引用此版本：0Mohammed Houssem Eddine Hachmaoui. SQL扩展的机械化和Coq认证翻译到嵌套代数.计算机科学编程语言 [cs.PL]. 巴黎-萨克雷大学, 2020. 法语. �NNT：2020UPASG021�. �tel-03026835�0博士学位论文0NNT：2020UPASG0210SQL扩展的机械化和Coq认证翻译到嵌套代数0巴黎-萨克雷大学博士学位论文0博士学位专业：信息与通信技术（STIC）博士学位580号，研究单位：巴黎-萨克雷大学，CNRS，计算机研究实验室，91405，奥赛，法国。参考人：奥赛科学学院0论文于2020年10月16日在吉夫-苏尔-伊韦特辩护和答辩，作者：0Mohammed Houssem Eddine HACHMAOUI0评审委员会成员：0Sophie Tison 主席0教授，里尔第一大学Alan Schmitt 评阅人和评委0研究主任，Inria雷恩研究中心Mohand-Saïd Hacid 评阅人0教授，里昂第一大学（LIRIS）Nicolas Tabareau 评委0研究主任，INRIA南特Nicolas Thiéry 评委0教授，巴黎-萨克雷大学0Évelyne Contejean 博士生导师0研究主任，CNRS（巴黎-萨克雷大学）Véronique Benzaken 博士生导师0教授，巴黎-萨克雷大学Chantal Keller 博士生导师0副教授，巴黎-萨克雷大学0在下一世，爸爸，我想再次成为你的孩子。0- Bernard Werber0献给我父亲的美好回忆。0致Habiba和Zinouna。nelle avec un nouvel opérateur pour la partie groupby having conçu spécifiquement pour prendre encompte tous les aspects de SQL cités précédem-ment. Ce même fragment de SQL, avec toute sessubtilités, est-il capturable par l’algèbre relation-nelle imbriquée ? Cette thèse prouve formellementque oui. En effet, nous proposons une traduction,certifiée en Coq, de SQLAlg vers NRAe, qui est uneformalisation en Coq de l’algèbre relationnelle im-briquée. La traduction prend en compte les expres-sions simples et complexes, les formules SQL etreflète parfaitement comment les environnementssont construits et manipulés, spécialement pourles agrégats et les requêtes corrélées. Ce travails’inscrit dans un cadre plus global, celui du pro-jet DBCert : une chaîne de compilation certifiéeen Coq de SQL vers JavaScript.Title : A Coq certified translation from an extension of relational algebra for SQL to a nestedalgebra.Keywords : Formalisation of data centric languages ; SQL’s formal semantics ; Certified compilation inCoq.Abstract : In 1974, Boyce and Chamberlin crea-ted SQL using the concepts of the relational alge-bra proposed by Codd in 1970, but as it evolved,its formal semantics became more and more com-plex. The small fragment select from where ofSQL can be mapped to a relational algebra, withbag’s semantics and by restricting expressions andformulae to those which can be expressed in re-lational algebra. To capture the semantics of themuch more realistic fragment select from wheregroup by having, taking into account all the ex-pressions including those with aggregates, all formsof formulas, null values and, even more subtle, thespecific SQL’s environments, Benzaken and Conte-jean propose SQLAlg which is an extension of rela-tional algebra with a new operator for the groupby having part designed specifically to take intoaccount all the aspects of SQL cited above. Canthis same fragment of SQL, with all its subtle-ties, be captured by nested relational algebra ? Thepresent work formally proves that the answer tothis question is yes. Indeed, we have built a cer-tified translation, formalized in Coq, from sqlalgto NRAe, which is a formalization in Coq of thenested relational algebra. The translation supportssimple and complex expressions, SQL’s formulaeand perfectly reflects how environments are builtand manipulated, especially for aggregates and forcorrelated queries. This work is part of a moreglobal framework : the DBCert project which isa compilation chain certified in Coq from SQL toJavaScript.Université Paris-SaclayEspace Technologique / Immeuble DiscoveryRoute de l’Orme aux Merisiers RD 128 / 91190 Saint-Aubin, France0标题：SQL扩展的机械化和Coq认证翻译到嵌套代数0关键词：数据中心化语言形式化；SQL的形式语义；Coq中的认证编译。0摘要：1974年，Boyce和Chamberlin基于Codd在1970年提出的关系代数创建了SQL语言，但随着扩展，SQL的形式语义与关系代数的形式语义越来越远。SQL的小片段select fromwhere可以对应于具有多重集语义的关系代数，通过将表达式和公式限制为关系代数可表达的那些。为了捕捉更加现实的片段select from where group byhaving的语义，考虑到包括带有聚合的所有表达式、所有形式的公式、空值以及更加特殊的SQL环境，Benzaken和Contejean提出了SQLAlg代数，它是关系代数的扩展。RemerciementsJe tiens à exprimer ma plus profonde gratitude et reconnaissance à :Mes encadrantes de thèse. Véronique Benzaken, Évelyne Contejean et Chantal Keller. Mercide m’avoir accompagné dans cette aventure scientifique et humaine. Merci pour vos conseils etvotre soutien.Les rapporteurs, Alan Schimtt et Mohand-Saïd Hacid. Je vous remercie d’avoir accepté derelire et de rapporter ma thèse ainsi que pour vos conseils et recommandations. Je remercieégalement Sophie Tison, Nicolas Tabareau et Nicolas Thiéry d’avoir accepté de faire partie de monJury.Louis Mandel, Jérôme Siméon et Avraham Shinnar, avec qui nous avons travaillé sur le projetDBCert.Je tiens également à remercier :Philippe Dhaussy et Alexandre Termier. Vous m’avez fait aimer la recherche. Merci!0Aammi Mohamed. Je te sais gré pour ta relecture du présent document et pour tes conseils.0Mes co-bureau, Hai et David. Mais aussi Pierre, Fabien, Georges, Marie et tous mes amis du LRI.0Les membres de l’équipe VALS et plus largement tout le personnel du LRI.0从小学到大学的所有老师们，感谢你们传授给我知识和生活的艺术。0最后，我要感谢并表达我永恒的感情给：0Maamar，Ramzi，Mohamed，Halim和Redouane以及我昨天和今天的所有朋友们。0我的妹妹Lamia和侄子Younès。我的兄弟Azzeddine，Ra�k，Chakib和Fakhreddine。我的整个家人。感谢你们在我整个旅程中的支持。0Adib和Rim。我的小家庭。你们与我一起分享了这段充满起伏的冒险。Adibou，在我写下这些文字的时候，你正坐在办公桌上。你开始了你的学校生活，我看着你成长。我为你感到如此幸福和骄傲。Rim，我爱你，简简单单。0我的母亲。谢谢你，妈妈！有了爸爸，我欠你们一切。xi0目录0第一部分：背景 10I 数据中心语言 30I.1 数据库的演变 . . . . . . . . . . . . . . . . . . . . . . . . . 40I.1.1 导航范式 . . . . . . . . . . . . . . . . . . . . . . . . 50I.1.2 关系范式 . . . . . . . . . . . . . . . . . . . . . . . . . . 70I.1.3 嵌套范式和对象范式 . . . . . . . . . . . . . . . 80I.1.4 半结构化范式 . . . . . . . . . . . . . . . . . . . . . . . 80I.1.5 NoSQL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90I.2 关系代数 (RA) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90I.2.1 关系模型 . . . . . . . . . . . . . . . . . . . . . . . . . . . 90I.2.2 关系运算符 . . . . . . . . . . . . . . . . . . . . . . . . 120I.3 SQL语言 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140I.3.1 SQL的数据模型 . . . . . . . . . . . . . . . . . . . . . . . 140I.3.2 数据查询语言 . . . . . . . . . . . . . . . . . . . . . . . . . . 150I.3.3 SQL的特点 . . . . . . . . . . . . . . . . . . . . . . . . . . . 180I.3.3.1 空值 . . . . . . . . . . . . . . . . . . . . . . . . 180I.3.3.2 关联查询 . . . . . . . . . . . . . . . . . . . . . 180I.4 嵌套关系代数 (NRA) . . . . . . . . . . . . . . . . . . . . . . . . . . . 210I.4.1 数据模型 . . . . . . . . . . . . . . . . . . . . . . . . . . . 210I.4.2 NRA运算符 . . . . . . . . . . . . . . . . . . . . . . . . . . 220I.5 RA、SQL和NRA的比较 . . . . . . . . . . . . . . . . . . . . . 250I.6 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 250II Coq认证编译 270II.1 形式化方法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 280II.2 证明助手 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 280II.2.1 Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 290II.3 认证编译 . . . . . . . . . . . . . . . . . . . . . . . . . . . 300II.3.1 定义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300II.3.1.1 编译 . . . . . . . . . . . . . . . . . . . . . . . . . . . 30xii0目录0II.3.1.2 编码和解码 . . . . . . . . . . . . . . . . . . . . 300II.3.1.3 语言机械化 . . . . . . . . . . . . . . . . . . 300II.3.1.4 代数编译器 . . . . . . . . . . . . . . . . . . . . 310II.3.2 一个代数编译器的修正 . . . . . . . . . . . . . . . . 310II.3.2.1 同构编码和解码 . . . . . . . . . . . . . . . . . . . 310II.3.2.2 同态编码 . . . . . . . . . . . . . . . . . . . 320II.3.2.3 同态解码 . . . . . . . . . . . . . . . . . . . 320II.3.3 Coq 中一个玩具语言的可证明编译 . . . . . . . . . . . . . . . . . . . 320II.3.3.1 语言 ToyExp . . . . . . . . . . . . . . . . . . . . . . . 330II.3.3.2 ToyExp 的实例化 . . . . . . . . . . . . . . . . . . . . 330II.3.3.3 ToyExpCert 的定义和证明 . . . . . . . . . . . . . . . . . . 330II.3.3.4 编译器 ToyExpCert 的实例化 . . . . . . . . . . . . . . . . . . . . 340II.4 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 350III SQL 和 NRA 的形式化 390III.1 SqlCert . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 400III.1.1 SqlCert 概述 . . . . . . . . . . . . . . . . . . . . . . . . . . 400III.1.2 SQL Alg ：RA的扩展 . . . . . . . . . . . . . . . . . . . . . . . . 410III.1.2.1 数据表示 . . . . . . . . . . . . . . . . . . . 420III.1.2.2 语法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 430III.1.2.3 查询示例 . . . . . . . . . . . . . . . . . . . . . 460III.1.2.4 SQL Alg 的环境 . . . . . . . . . . . . . . . . . . . . . . . 460III.1.2.5 语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . 490不带聚合的表达式语义 . . . . . . . . . . . . . . . . . . . 500带聚合的表达式语义 . . . . . . . . . . . . . . . . . . . 510公式的语义 . . . . . . . . . . . . . . . . . . . . . 520查询语义 . . . . . . . . . . . . . . . . . . . . . 530III.1.2.6 概念验证：一个规范实例 . . . . . . . . . . . . . . . . . 540III.2 Q*Cert . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 570III.2.2 NRA e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 570III.2.2.2 NRA e 语法 . . . . . . . . . . . . . . . . . . . . . . . 580III.2.2.3 NRA e 的语义 . . . . . . . . . . . . . . . . . . . . . . 600III.3 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 620第二部分：贡献 650IV 从 SQL Alg 到 NRA e 670IV.1 目标和方法概述 . . . . . . . . . . . . . . . . . . . . . . . . . . 680IV.1.1 翻译目标 . . . . . . . . . . . . . . . . . . . . . . . . . 680IV.1.2 翻译总体概述 . . . . . . . . . . . . . . . . . . . . . . . . . 690IV.2 数据模型的编码 . . . . . . . . . . . . . . . . . . . . . . . . . . 70xiii0目录0IV.2.1 值的编码 . . . . . . . . . . . . . . . . . . . . . . . . . . . 710IV.2.2 属性名称的编码 . . . . . . . . . . . . . . . . . . . . . . 710IV.2.3 三值逻辑的编码 . . . . . . . . . . . . . . . . . . . . 710IV.2.4 元组编码 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 720IV.2.5 集合编码 . . . . . . . . . . . . . . . . . . . . . . . . . . 730IV.2.6 数据编码总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . 740IV.3 数据库实例编码 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 740IV.4 编码和环境管理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 750IV.5 SQL Alg 的翻译 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 790IV.5.1 表达式 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 790IV.5.1.1 简单表达式 . . . . . . . . . . . . . . . . . . . . . . 800IV.5.1.2 复杂表达式 . . . . . . . . . . . . . . . . . . . . . 830IV.5.1.3 命名表达式列表 . . . . . . . . . . . . . . . . . 850IV.5.2 公式 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 850IV.5.2.2 三值逻辑NRA e的运算符 . . . . . . . . . . . 870IV.5.3 查询 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 890IV.5.4 翻译示例 . . . . . . . . . . . . . . . . . . . . . . . . . . 920IV.6 规范的实现 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 920IV.6.1 空值 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 930IV.6.2 三值逻辑的值 . . . . . . . . . . . . . . . . . . . . . . . 940IV.6.3 函数符号 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 950IV.6.4 聚合符号 . . . . . . . . . . . . . . . . . . . . . . . . . . . 960IV.6.5 谓词符号和逻辑运算符 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 960IV.7 翻译的修正定理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 980IV.8 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1010第三部分：讨论 1030V 讨论 1050V.1 应用案例：DBCert . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 V.1.1 DBCert的介绍 . . . . . .. . . . . . . . . . . . . . . . . . . . 1050V.1.2 语义保持性 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1060V.1.3 示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1060V.1.4 DBCert的评估 . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 V.1.4.1 AlaSQL . . . . . . . . . . .. . . . . . . . . . . . . . . . . . 1080V.1.4.2 基准测试 . . . . . . . . . . . . . . . . . . . . . . . . . . . 1080V.1.4.3 结果 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1090V.1.4.4 性能 . . . . . . . . . . . . . . . . . . . . . . . . . . 1100V.2 相关工作 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110xiv0目录0结论和展望 1150参考文献 1160附录 1250A 附加材料 1250B SELECT查询的语法 1270C NRA的操作语义 e 1290D 参数化的SQL Alg 规范 1310图表目录0I.1 示例：一个层次数据库的例子。 . . . . . . . . . . . . . . . . . 70I.2 关系数据库的示例。0I.3 集合投影与多重集合投影的比较。0I.4 SQL的select from where group by having片段的语法。0I.5 关联查询的示例。0I.6 NRA模型中的关系示例。0I.7 应用group by的示例（NRA）。0II.1 根据[Mosses，1980]的编译修正。0II.2 根据[Thatcher等人，1980]的编译修正。0II.3 根据[Morris，1973]的编译修正。0II.4 ToyExp语言的规范/定义。0II.5 ToyExp语言的实例化。0II.6 定义和验证ToyExpCert。0II.7 ToyExpCert编译器的实例化。0III.1 SQL Coq的语法。0III.2 泛型模型参数化SQL Alg的Coq形式化。0III.3 SQL Alg表达式的语法。0III.4 泛型参数化SQL Alg表达式的函数和聚合。0III.5 SQL Alg公式的语法。0III.6 泛型参数化SQL Alg公式的谓词。0III.7 SQL Alg查询的语法。0III.8 SQL Alg的环境示例。0III.9 找到带有聚合的表达式的正确评估环境的函数的语义。0III.10 NRA e的数据模型。0III.11 在Coq下定义NRA e的数据模型。0III.12 NRA e的语法。0IV.1 翻译的架构。0IV.2 在Coq中规定数据模型的编码。0xv0图表目录0IV.3 在Coq中规定三值逻辑的编码。0IV.4 在Coq中定义元组的编码。0IV.5 在Coq中定义元组的多重集编码。0IV.6 在Coq中规定数据库实例的编码的规范和定义。0IV.7 提取环境的抽象部分。0IV.8 在Coq中定义SQL Alg环境的具体部分的编码的规范和定义。0IV.9 定义push函数，将一个切片添加到当前环境中。0IV.10 在Coq中规定函数符号的翻译的规范。0IV.11 简单表达式翻译的Coq规范........................................820IV.12 聚合符号翻译的Coq规范........................................830IV.13 带聚合表达式的正确翻译环境的函数语义........................................840IV.14 命名表达式翻译的Coq定义........................................850IV.16 NRA逻辑和SQL Alg查询翻译的Coq规范........................................880IV.17 SQL Alg公式翻译........................................890IV.18 SQL Alg查询翻译........................................910IV.19 Coq中用于SQL Alg查询翻译的所有必要元素的规范..........................................920IV.20 实例的模式表示........................................930IV.21 值编码实现..........................................940IV.22 三值逻辑编码的实现........................................950IV.23 in B运算符定义........................................990IV.24 翻译模拟图........................................990V.1 DBCert项目架构........................................1060xvi0第一部分：0背景0这篇论文处于数据中心化语言和形式化方法的交叉点上。尽管形式化方法在不同的研究和应用领域为关键软件的正确性提供了保证，但它们在形式化和研究数据中心化语言和系统方面却很少被使用。0在将这两个领域结合起来的最成功的研究工作中，SqlCert [Benzaken etContejean，2019]和Q*Cert [Auerbach etal.，2017d]使用Coq证明助手来形式化和研究数据中心化语言。0我们的研究工作通过在Coq中提供了一个从SqlCert中的语言到Q*Cert中引入的语言的认证翻译，将这两个项目联系起来。0在本部分中，我们介绍与本论文相关的数据中心化语言，特别关注与之相关的语言。然后，我们通过介绍形式化方法和Coq证明助手的方法来介绍所使用的方法。最后，我们介绍了前面提到的两个项目，这两个项目是我们工作的基础。0这部分将我们的论文放入背景中。出于教学目的，现有的内容在引言和解释不同概念和概念的过程中逐渐被引用。这个选择是由我们的论文定位在多个研究领域的交汇处所决定的。相关的其他补充工作将在V.2中讨论。相关工作。I.1.5NoSQL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .930章节0我0数据中心化语言0这篇论文是在数据中心化语言形式化的框架下进行的。这些语言专门用于数据处理。它们通常是声明性的。在本章中，我们关注数据模型和处理它们的语言的演变。我们特别关注关系代数[Codd，1970]，它是参考语言，然后是SQL，它在语义上与我们在本论文中提出的认证翻译的源语言是等价的。最后，我们还介绍了NRA语言，它在语义上与我们的翻译目标语言是等价的。0I.1 数据库的演变 . . . . . . . . . . . . . . . . . . . . . . . . . 40I.1.1 导航范式 . . . . . . . . . . . . . . . . . . . . . . . 50I.1.2 关系范式 . . . . . . . . . . . . . . . . . . . . . . . . . 70I.1.3 嵌套范式和对象范式 . . . . . . . . . . . . . . . . . . . . . 80I.1.4 半结构化范式 . . . . . . . . . . . . . . . . . . . . . 80I.2 关系代数（RA） . . . . . . . . . . . . . . . . . . . . . . . . . . 90I.2.
我的内容管理
展开
