形式化系统设计：描述和操作操作语义的研究

T Hesa德博士学位L’UNIVERSITÉ DE RENNES和科尔 D八角形第601章数学与信息与通信科学与技术由路易斯·诺伊泽Necro：没有骨头的用于描述和操作操作语义的形式化系统的设计论文于2022年9月29日在雷恩提交并答辩研究单位：IRISA答辩前的报告员：Jean-Christophe FILLIATRE CNRS研究总监Jean-Bernard STEFANI格勒诺布尔Inria研究总监评审团组成：主席：大卫·贝尔德雷恩高等师范学校高级讲师检查员：尚塔尔·凯勒阿西娅·马赫布比巴黎萨克雷大学副教授Inria NantesDir.论文：扬·雷吉斯-吉安娜·艾伦·施密特Nomadic LabsInria Rennes2TABLE从材料引言6什么形式语义的重要性6如何定义语义7论文结构8执行情况91背景101.1定义101.1.1大步骤111.1.2小步骤121.1.3抽象机器131.2等效性151.3语义描述语言152骨架和骨架语义学252.1例25中的骨骼2.2形式主义302.3存在主义322.4多态性332.5Skel34中的单子2.6打字362.7具体解释372.7.1值集372.7.2推理规则2.7.3推理规则2.7.4主题简化和进展472.8抽象解释482.8.1值集482.8.2评估522.8.3一致性5533NecroLib563.1 AST. ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...563.1.1类型skeleteal_semantics。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ...563.1.2术语和骨架类型。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...583.1.3类型necro_type。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ...603.2词汇和句法。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...613.3类型。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... ... ...613.4转型。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ...633.4.1解释。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ...633.4.2变压器。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...643.4.3应用程序。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ...654NecroML674.1生成的文件。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...674.2解释的单子... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...742.1单子恒等式。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...754.2.2单子列表。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...764.2.3延续。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...774.2.4BFS。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...784.2.5单子BFSYield。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...814.2.6单子。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...822.7其他单子834。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...4.2.8评估。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ...834.3实例化。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ...845Necro公鸡875.1结构。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ...875.2Skel。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ...885.3打字。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... ...895.4价值观。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... ...905.4.1基本。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...905.4.2未规定的功能。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...915.5解释。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ...925.5.1大台阶，感应式版本。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...925.5.2大步，迭代版本。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...935.5.3小步。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .945.5.4抽象。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...955.5.5主题缩减。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...955.6实际示例。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...955.6.1析因计算的证明... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...9555.6.2语义等价性证明5.7应用程序和易用性6其他工具和未来工作1026.1Necro调试1026.2模块化1036.3Necro103的外部使用6.4未来工作1047结论105附件107A.1λ-无评估策略的计算A.2多态性1096REMERCIENTS我们一个人走得更快，我们一起走得更远非洲谚语按照惯例，我想在开始这篇论文时感谢所有帮助我得出这里所产生的结果的人最重要的是，我感谢艾伦的耐心，他的幽默，他的好建议，并设法支持我在3年的论文，尽管生产力相当不平衡。我感谢报告员和审稿人同意参加我的论文评审我衷心感谢凯尔特团队在过去三年中举办的丰富的研讨会，感谢你们在我的演讲中有趣而宝贵的发言，感谢你们在咖啡、茶或热巧克力中度过的美好时光（特别是在新冠肺炎然后，我要感谢我参加的会议的发言者我想特别感谢塞缪尔，感谢他把Necro放在opam上，但也许最重要的是，感谢他在感谢亚当，当我需要找一个新家的时候，他把感谢我的家人，他们特别要感谢托马斯、圣地亚哥和卡里贝，他们感谢雷恩市的比萨饼店，特别是已故的Pizz感谢所有在法国童子军和向导中指导和陪伴我的人。C’est grâce à mes expériences SGDFque j’ai acquis de nombreuses qualités humaines, qui最后，非常感谢Santiago、Jade、Jean-Loup、Roméo、Théo和Vincent准备了一个非常高质量的论文，主要是素食主义者。7一、引言[P]ripensuboneantalego：tutene estas mi alituda，foretumin，撤回葡萄酒通过Dika sel Testuda。彼得·佩内特Sekretaj Sonetoj什么语义学是赋予单词、句子和语言以意义。C’est ce qui nous例如，如果我们想象一下，如果你的邻居用独角兽这个词来形容犀牛，你可能不会把它当回事，如果他说："小心，独角兽正在向你扑来!"»词典保证了词的语义的某种连贯性，但是语言的演变和词典的多样性使得语义的完美统一成为因此，根据地区的不同，同事不一定和你一起工作，口袋也某些单词和短语的这种多义性可能会导致严重的混淆如果你邀请一个魁北克人共进晚餐，你可能会惊讶地看到他们在中午到达你的家。同样，如果我们对单个单词的含义达成因此，当两个人交流时，重要的是要确保两个人使用的单词的语义是明确的形式语义的重要性当涉及到计算机时，问题是一样的。如果您通过用任何与您的1. 例如，在写这篇论文的时候，小罗伯特承认了"iel"这个词，而大多数词典，特别是法兰西学院的词典，8您希望计算机了解您要执行的操作如果你要求你的手机在第二天早上7点叫醒你，闹钟当然，醒得太早或太晚似乎已经不受欢迎了，但还有更关键的情况。由地铁紧急停止控制器激活的程序、操作心脏起搏器的软件或操作核电站的软件都是其故障引起严重问题的为了确保你的程序做你期望它做的事情，你必须已经理解了你所使用的因此，我们必须为这种语言提供清晰而独特的语义为计算机语言提供语义比为自然语言提供语义要简单得多，原因如下— 计算机语言通常比自然语言受到更少— 这些发展通常由负责语言的组织（通常是最初创造语言的组织）进行编码和选择— 计算机语言使用很少的单词，这些单词的语法比普通语言简单得多尽管有这种表面上的简单性，但很少有语言有明确的语义大多数情况下，语言被认为是足够明确的，没有语义，有时解释器作为一个参考。缺乏正式的语言定义是一个明显的问题，因为如果代码是用不正确指定的语言编写的，则代码可能不适合所但还有第二个更微妙的问题。如果一个因此，用源语言编写的代码的语义和由编译器翻译的代码的语义不一定是一致的。如何定义语义既然读者已经确信指定所使用的语言的语义的重要性，那么我们就来某些规范是用人类语言编写的 此语义允许您9它是有意义的程序，但不是机械化的，也就是说，它不是用计算机可以理解的语言编写的，这意味着几个— 语义中可能存在错误，并且可能难以检测到这些错误。— 通常有未经验证的断言（ECMA-262通常会做出2个断言，这些断言被构造为真）。— 无法从规范中执行代码。— 在计算机上证明程序的正确性是不可能的。D’autres并能够用计算机证明代码的某些属性存在几种用于以计算方式定义语义的工具最标准和最常见的方法是使用证明助手，这些语义通常是不可执行的，因此必须被提取到另一种这种方法相对有效，但设计选择的改变，如从浅浸到深浸，通常会有很因此，我们通常更喜欢一种规范语言，它将建议提取到一个证明向导，一种可执行语言，如果需要的话，现有的工具有Lem、Ott和K，它们都有自己的局限性，我们将在1.3节中介绍它们。本文介绍了Skel语言，一种轻量级而强大的规范语言，以及Skel语言的更新以及论文的结构本论文报告由7个部分组成在第1节中，我们将语义，特别是操作语义置于它们的上下文中，这是相当迅速的。第二部分描述了Skel语言是如何工作的，目前的版本是本文的贡献第3节、第4节和第5节分别介绍了Necro Lib、Necro ML和Necro Coq工具，这些工具是在本论文的框架内构建的。最后，2. https://262.ecma-international.org/12.0/#assert10第6节介绍了实施工作Necro Lib几乎完全是在本论文的框架内实现的，总共有5000多行代码。Necro ML代表了1300多行代码和1000多行测试。Necro Coq包含几行代码（300多行），这证明了创建一个工具是多么容易。使Necro Coq翻译的语义工作所需的Coq文件有2000多行。在本论文的框架内，对这些文件进行的证明总共增加了3000行。而在这篇论文中进行的测试又多了800行Necro Debug总共有1800行代码。在这篇论文的框架内，总共编写了超过10，000行代码当然，这些行只是3年研究工作的最终结果所开展的工作还导致多次参加会议。我们在2020年和2021年的法语应用语言日上发表了两篇文章[20，13]，并在ICTCS 2022上发表了一篇题为"统计和处理语义学"的文章。最后，关于这些工具的易用性，它们是由Samuel Risbourg在一个非官方的opam存储库中提供的，可以通过执行以下命令来安装所有这些工具，以便能够在阅读本论文的同时进行Opam更新opam开关创建necro 4.14.0 opam开关necroeval $（opam环境）opam存储库添加necro https://gitlab.inria.fr/skeletons/opam-repository.git#necro opam安装-y necrolib necroml necrocoq necrodebug11C第1章C.反文本这是尼尔·阿姆斯特朗1.1定义为了能够对程序进行推理并证明它们的属性，能够给出所述语言的语义是至关重要的我们将通过一个简单的例子来说明这一部分，即IMP语言在下文中，我们将主要使用λ-演算作为支持，但这种命令式语言的例子更完整，因此可以立即显示更多的概念，并更好地IMP语言的语法如图1.1所示。加法运算符、否定运算符、相等运算符以及整数和布尔常量都用一个点标记，的确，8 是unentier，+是用于编写IMP表达式的语法给出一种语言的语义预期结果的类型例如，对于IMP语言，表达式根据值（值为整数或布尔值）进行求值，而指令根据内存状态进行求值至少有三种主要的方式来给出语言的语义- 指称语义为每个程序提供了一个指称。此指示通常是一个函数，它将输入作为参数（在经验Re：：=n|⊥˙|⊤˙|x|E+E|e=e|eSTMTs：：=跳过|x：=e| s; s|如果是S|而SFIGURE 1.112{P × b}s{P}{P}而b s{P> b}图1.2σ，eeσ，s1sσ′，如果e s1s2sσ′σ，eeσ，s2sσ′，如果e s1s2sσ′图1.3IMP，— 公理语义学使用霍尔逻辑来证明形式为{P}s{Q}的霍尔三元组。这些三元组确保它要求"猜测"与证明最终结果相关的命题。例如，对于while块，我们需要找到— 另一方面，操作语义更接近于计算机执行程序的方式给定一个状态和一个表达式，它会给出结果，通常带有一个归纳定义，该定义将把不同的执行步骤作为参数在下文中，我们将集中讨论操作语义有几种方法可以给出语言的操作语义小步骤语义解释了如何执行单个计算步骤，并且可以语义学使用归纳规则直接给出结果，这是一个巨大的飞跃1.1.1大步一个大的语义步骤归纳地定义了达到一个结果所需的计算。因此，它将表达式（通常是上下文或状态）作为参数，并直接返回值。图1.3给出了if的大步长语义的两个规则你可以看到规则一下子就做到了。它计算条件，选择正确的语句并对其进行评估。图1.4给出了IMP大步语义的所有规则。13ADDσ，nenC第一次σ，eTOPσ，eBOTσ（x）=v vVσ，xe vσ，e1en1σ，e2en2n1+n2=nσ，e1+e2enσ，e1en σ，e2enEqT街道σ，e1=e2eσ，e1en1σ，e2en2n1=n2EqFALSEσ，e ebNEGσ，跳过sσS基普σ，e1=e2eσ，eevANNσ，x：=esσ[x ← v]是啊，是啊σ，s1sσ′，s2sσ′SE q（s1;s2）sσ′σ，ee σ，s1sσ′IF T街σ，eeδ σ，s2sσ′IF FALSE（如果是1，则为2），（如果是1，则为2）σ，ee σ，ssσ′σ′，（当e s）sσ′WHILE TRUEσ，ee e WHILEFALSE（当s）sσ′，（当s）sσ图1.4下面是在执行ndd e l a时为m ul e x +（y +2）在s状态下推导nc e ass o的sr规则σ，其中x与1相关联，y与3相关联：σ（y）=3σ（x）=1V型V型σ，ye3σ，2C第一次23+2=5DDσ，xe1σ，y+2e5σ，x+（y+2）e61+5=6DD1.1.2小步另一方面，在小步语义中，我们一步一步地分解步骤因此，我们计算一个步骤并返回一个新配置，该配置是在计算步骤之后获得的为了能够在每个阶段之后重建配置计算完成后，将使用仅包含一个值的配置。当计算开始时，使用状态和要计算的表达式或语句。但是对于一些制造商，我们必须添加新的制造商来存储中间数据。例如，对于+，我们需要在计算第一个表达式时存储该表达式的值我们从Doncav开始，用la和e两个x表达式，av用llconstucteurinitial+，de签名E14经验Re：：=n|⊥˙|⊤˙|x|E+E|v+e|e=e|v=e|eSTMTs：：=跳过|x：=e| s; s|如果是S|而SFIGURE 1.5expr * expr → expr. 然 后 ， 当 第 一 个 表 达 式 计 算 为 整 数 值 时 ， 我 们 使 用 构 造 函 数 +，deint*expr→expr签名。最后，当两个表达式的计算完成时，我们将它们扩展语法见图1.5。我们在图1.6中给出了IMP的小步长语义的所有规则，并在下面扩展了s三个步骤s e x +（y + −2）在s e与前面n t相同的状态σ下的值σ（x）=1V型σ，x −→e1ADD LR和σ，x+（y+2）−→eσ，1+（y+2）σ，y −→e3ADD LR和σ，y+2-→eσ，3+2ADDRC有σ，1+（y+2）−→eσ， 1+（3+2）σ，2−e2DDRR和σ，（3+2）−→e5DDRR和σ，1+（3+2）−→e 6因此，我们有：σ，x+（y+2） −eσ，1+（y+2）−eσ，1+−（3+−2−）-E61.1.3抽象机器为了避免必须重建项的问题抽象机器是一种评估方法，其中选择要评估的术语部分，并将上下文保存在内存中以供以后使用因此，评估配置IMP的抽象机器语义的所有规则如图1.7所示。15σ，n→enC第一次σ，-→eTOPσ，−eBOTσ（x）=vσ，x−→evV型σ，e1−→e_，e′1σ，e1+e2−→eσ，e′1+e2σ，e2−→e_，e′2σ，n1+e2−→eσ，n1+e′2σ，e1−→e_，e′1DDLC有一个DDRCEqLC有σ，e1−→en1ADD LR和σ，e1+e2−→eσ，n1+e2σ，e2−→en2ADD RR和σ，n1+e2−→e（n1+n2）σ，e1−→en1EqLR和σ，e1=e2−→eσ，e′1=e2σ，e2−→e_，e′2σ，n1=e2−→eσ，n1=e′2EqRC有σ，e1=e2−→eσ，n1=e2σ，e2−→enEqRR和 T街σ，n=e2−→eσ，e2−→en2n2=n1EqRR和 F也是σ，e−→eσ，e′NEG C有σ，n1=e2−→eσ，跳过−→s σσ，e-→eσ，e'σ，e −→ebNEG R和σ，e-→bσ，x：=e −→s（σ[x ← e]）σ，s1 −→s σ′，s′1[1][2][3][4][5][6][7][8]S和 QLCσ，s1−→sσ′[1][2][3][4][5][6]QLR和σ，e −→e_，e′σ，（如果e′ s1s2）−→sσ，（如果e′s1s2）IF LC有σ，e −→eIFLR和 T街σ，（如果e是1，s是2）−→sσ，s是1σ，e −→eIF LR和FALSEσ，（如果e是1，s是2）−→sσ，s是2σ，（whilees）−→sσ，如果e（s;whilees）跳过W希尔S基普一个SN16图1.617有两种模式。计算模式（用V形符号表示）和继续模式（用方括号表示），前者表示表达式正在计算中，后者表示已经有值并正在我们演示了如何在σ状态下计算相同的表达式x+（y +2）。因此，我们有：

下载后可阅读完整内容，剩余1页未读，立即下载