0博士学位论文0雷恩第一大学0第601号数学与信息与通信技术学院专业：计算机科学0Guillaume AMBAL0骨架语义转换0博士论文于2022年10月19日在雷恩进行，研究单位：IRISA (UMR6074)0答辩前的评审人：0Dariusz BIERNACKI 副教授 — Wrocław大学，波兰 Christine TASSON 教授 —Sorbonne Université，巴黎0评审委员会成员：主席：Nathalie BERTRAND 研究主任 — Inria Rennes 评审人：Dariusz BIERNACKI 副教授— Wrocław大学，波兰 Christine TASSON 教授 — Sorbonne Université，巴黎 Daniel HIRSCHKOFF 讲师 —LIP，ENS de Lyon Jean-Marie MADIOT 研究员 — Inria Paris 博士导师：Alan SCHMITT 研究主任 — InriaRennes 博士共同导师：Sergueï LENGLET 讲师 — Lorraine大学，南锡.................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................Muxu.30致谢0感谢我的导师和博士共同导师指导我到这一步。0感谢评审人抽出时间阅读这篇论文。0感谢Platypus列表的所有成员进行的讨论和晚会。0感谢我的家人对我的支持和奇异果。0感谢我的妹妹为她的混乱和任性的灵感。e ::= x | n | Plus(e1, e2) | . . .c ::= skip | while e do c | . . .syntaxe ci-dessus, on définit les règles suivantes.s(x) = ns, x ⇓ s, ns, e1 ⇓ s1, n1s1, e2 ⇓ s2, n2n1 + n2 = ns, Plus(e1, e2) ⇓ s2, n. . .s, e ⇓ s1, trues1, c ⇓ s2s2, while e do c ⇓ s3s, while e do c ⇓ s3s, e ⇓ s1, falses, while e do c ⇓ s150法文摘要0语言和语义0在计算机科学中，算法和软件的开发是通过使用编程语言来完成的。0编程。这些语言间接地实现了程序之间的通信。0因此，在计算机科学中，形式化定义这些语言变得至关重要，以避免人与机器之间的解释问题。0人与机器之间的解释问题。0语言的定义由 语法 和 语义 组成。语法表达了0哪些对象被视为有效的程序，并且可以很容易地进行形式化。0使用语法来定义。例如，假设存在变量 ( x ) 和整数 ( n )，0可以使用以下语法来定义表达式 ( e ) 和程序 ( c )：0然后，语言的语义赋予这些程序以意义。在本文档中，0我们专注于操作语义，其中程序被解释为一个程序。0作为计算序列的一部分。因此，操作语义解释了如何执行程序。0操作语义的形式化可能是棘手的。对于上述的语法，我们定义以下规则。0在计算机语言中，最好使用无歧义的推理规则。对于0评估 Plus ( e 1 , e 2 ) 的过程是先评估 e 1 和 e 2 ，然后将结果相加。0要评估 while e do c 循环，首先评估条件 e ；如果结果为真，则0在循环 while e do c 中，先计算命令 c ，然后循环。否则，停止计算。0对于更复杂的语言，推理规则可能会很冗长且0很难阅读、编写和修改。因此，通常会以0通过英语解释来定义。因此，并非所有语言都具有相同的type identtype expr =| Var ident| Plus of expr * expr| ...type stmt =| Skip| While of expr * stmt| ...val add : ...hook hexpr (s: state, e: expr) matching e =| Var (x) -> ...| Plus (e1, e2) ->let (s1, n1) = hexpr (s, e1) inlet (s2, n2) = hexpr (s1, e2) inlet n = add (n1, n2) in(s2, n)| ...60精确的描述。例如，JavaScript的语义非常详细，可以看作是0推理规则的英文翻译，而Python的文档是0更高级别的行为描述。0这些非正式定义限制了语言语义的可能用途。0编程语言的语义通常以非正式的方式描述。它们通常用于0相反，计算机上的机械化语义可以作为参考来证明0语言的属性，或者用于验证相关工具，如解释器或调试器。0调试器。0这种机械化可以在通用软件中完成，例如助手0证明（Coq [52]，Isabelle [39]，...）或使用专门的工具，如K [48]和语义0骨架语义[17]。在本文中，我们使用骨架语义来实现0非常简单地操作语义。0骨架语义0骨架语义是一种用于形式化操作语义的逻辑框架。0使用名为Skel的小型元语言来形式化编程语言的语义。0语言的语义由用Skel语法编写的对象表示。该定义可以0可以将其视为代码片段（元语言）或解释器。这使得0更容易编写、阅读和操作。这样的定义变得正式起来。0通过Skel元语言的语义规则间接地实现了清晰且无歧义的语义。0推理规则。0Skel元语言被设计成具有很高的骨架语义模块化性。0同时保持基本操作的行为抽象（比较两个整数、0评估操作（操作序列、递归调用、非确定性分支等）。0而不受基本操作实现选择的影响。0更新环境等）。因此，可以分析、转换或0可以独立地对其进行认证，而不受基本操作实现选择的影响。0例如，我们可以用以下方式形式化前面的小语言：sémantiques à grand pas sont les plus intuitives et les plus répandues, mais ne peuvent pas70因此，保持了评估 Plus ( e 1 , e 2 ) 的思想，即连续评估 e 1 和 e 2 （通过0递归调用），然后将结果相加。这与0add ）进行加法运算。0骨架语义及其在OCaml中的实现[36]称为Necro[21]，0然后可以自动处理这些定义。不同的工具可以实现0将语言导出为Coq定义，或自动生成解释器和0从语义生成调试器。0骨架语义的框架逐渐丰富，本文涵盖了0两个不同版本的Skel元语言。主要区别是版本0本文第一部分使用的语义框架不允许高阶函数。0贡献0存在不同的操作语义格式。例如，有一些语义-0大步语义将程序与其最终结果相关联，小步语义-0明确中间计算，并详细说明抽象机的0处理不同元素的方法。每种格式都有其优点和缺点。0无法使用其他类型的语义来描述所有可观察的行为。根据0大步语义是最直观和最常见的，但不能0相同语言的语义。0为了验证所需的属性，有时需要处理多个版本的0在需要更多工作的同时，必须确保所有不同的定义都是0然而，手动多次形式化相同的语言并不理想。此外0从一个定义生成所有这些定义，尽可能提供最多的保证。本文0等效的。因此，最好开发系统化的方法来生成0用户语言和Skel元语言。0深入研究了操作语义的相互推导，既在0本论文的第一部分介绍了一种新的方法，可以自动转换0将大步语义自动转换为小步语义0等效的。0这个小步转换的主要困难是创建新的构造器。0构造器。实际上，初始语法通常不足以表达计算0在评估过程中可能出现的中间计算。通常情况下会出现这种情况0当一个参数需要被多次评估时。例如，对于构造器0Plus(e1，e2)，推理规则以前提s，e1 � s1，n1开始。在小步中，如果80以前提s，e1 → s'，e'1开始计算e1时，可以轻松覆盖0e1的初始值。因此，我们的方法生成以下规则。0s，e1 → s'，e'10s，Plus(e1，e2) →s'，Plus(e'1，e2)0对于构造器while e do c，无法有类似的规则。如果0开始用前提 s，e 评估 e，e → s'，e'，我们不能覆盖初始值0e与e'，因为我们可能需要稍后重新评估while e do c。转换0然后扩展语法，并引入一个新的构造器（称为 While1 ），能够存储0所需的中间结果。0这个转换分为几个步骤。特别是，有一个分析阶段-0该阶段使用这些新构造器生成逐步语义。0运行语义以确定程序中需要添加新构造器的位置。0该阶段使用这些新构造器生成逐步语义。0还重要的是验证该算法是否正确，即新构造器是否正确生成。0输出的逐步语义与提供的大步语义是等价的。0由于分析阶段复杂且容易优化，完整版本的转换不适合直接进行认证。0该算法的完整证明不适合直接进行认证。因此，我们开发了一种简化版本的证明。0我们使用了两种不同且互补的方法来确保转换产生了预期的结果。0预期的结果。0首先，我们提供了一份论文证明，证明了不经过分析的转换是正确的。0实际上，这个简化版本的逐步语义不如优化版本的逐步语义。0使用比必要构造器更多的构造器。数学证明保证了策略的正确性。0基本证明在所有语言上都是有效的。0然后，为了证明完整版本的实现，我们还生成了每种语言的Coq证书。0为每种语言生成一个Coq证书，证明输入语义和输出语义之间的等价关系。0Necro可以生成两种语义的Coq定义，以及已知的策略。0等价证明的生成不依赖于这些语义。因此，我们可以生成任何感兴趣的语言的等价证明。0为每种语言生成一个专门的Coq证明脚本。这种事后认证方法可以验证实现的正确性。0既可以直接在我们感兴趣的语言上保证等价性，也可以在最终版本上保证等价性。0不必担心实现中的错误，因为我们只验证结果是否正确。0最终版本。0将这个转换与Necro环境结合起来，我们还可以生成任何语言的解释器。0自动生成任何语言的逐步解释器。90元语言的新语义。0由于语言的骨架语义是用Skel元语言编写的，它只能通过元语言的语义来理解。0元语言的语义。0大步非确定性解释，称为具体解释。虽然对于许多程序分析任务来说很有用，但它不能执行程序。为了解决这个问题，我们提出了一种称为功能对应的技术。0在语言和程序的证明中，具体解释不能提供任何有关语言的信息，只能通过元语言的语义来理解。Skel是通过一个具有非确定性和确定性的大步语义来定义的。0从具体解释中推导出功能对应。这是一种从具体解释中推导出功能对应的技术。0为此，我们提出了两种新的Skel解释，以抽象机器的形式表示。0确定性和非确定性。0我们不是手动创建这些新的语义，而是使用技术生成它们。0从具体解释中使用功能对应技术推导出的技术。这是一种从具体解释中推导出功能对应的技术。0从一个大步语义中推导出一个抽象机器的系统方法。0它结合了多种已知的转换，逐步重写语义。0以可中断的形式。0由于具体解释是非确定性的，将其应用于功能对应是可中断的。0通过这种方法，我们可以得到一个等价的非确定性抽象机器。这个新的抽象机器是通过将原始语义转换为一个更简单的语义来实现的。0新的语义很有趣，但仍然无法执行程序。0实用。为了创建确定性的抽象机，我们使用了更复杂的0功能对应关系的抽象语义。这涉及在0语义的非确定性部分，允许执行在遇到问题时回退0问题。因此，我们得到了一个确定性和可执行的元语0Skel语言。这个抽象机相对于具体解释是正确的0机器得到一个结果时，这个结果是正确的。然而，并不是所有的结果0正确的不一定是可访问的0这两个抽象机（非确定性和确定性）在0我们使用Coq证明了这两个新的语义是有效的0分别等价和相对于具体解释是正确的0我们还使用Coq的提取系统获得了OCaml版本0确定性抽象机的可执行版本，执行Skel元语言。通过使用0使用Necro工具，该机器可以自动实例化为任何0骨架语义提供了一个经过验证的解释器0Skel0手稿的计划0本文档的第2节介绍了主要的操作语义形式0大步语义，小步语义，规约语义和抽象机0第一部分介绍了一种自动转换骨架语义的策略100大步骨架语义转换为小步骨架语义。这个转换是0在早期版本的Necro中实现了这个转换，用于没有函数的骨架语义0高阶骨架语义的版本稍微简化的证明0转换的正确性。我们没有证明算法的完整版本，但是0对于每个使用，我们生成一个结果保证。因此，实现0自动生成等价的小步语义和Coq脚本验证0这个等价性0本手稿的第二部分集中讨论语义骨架元语言（Skel）0当前高阶骨架语义。我们使用已知的方法转换0并生成确定性和非确定性抽象机0Skel的非确定性版本。我们在Coq中证明了非确定性版本与0起始语义，而确定性版本相对于起始语义是正确的0大步语义。提取确定性版本使我们获得了一个经过验证的解释器0任何在Skel中定义的语言110目录01 引言 1601.1 贡献 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1701.2 文档的组织结构 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1902 操作语义 2002.1 IMP的语法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2002.2 大步语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2102.3 小步语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2302.4 归约语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2802.5 抽象机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3002.6 互补推导 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 340I 对象语言转换 3703 骨架语义 3803.1 示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3803.2 Skel的语法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4103.3 具体解释 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4203.4 无穷解释 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4503.5 Necro . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4504 小步转换 4704.1 一个示例的概述 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4704.1.1 强制转换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4704.1.2 新构造函数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4804.1.3 使骨架小步 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5004.2 形式化转换阶段 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5304.2.1 强制转换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5304.2.2 新构造函数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5404.2.3 分布分支 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6004.2.4 使骨架小步 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61120目录05 转换的认证 6605.1 纸笔证明 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6605.1.1 证明概要 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6705.1.2 转换属性 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6805.1.3 初始和扩展大步语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . 7005.1.4 小步推导导致扩展大步推导 . . . . . . . . . . . . . . . . . . . . 7005.1.5 扩展大步推导导致小步推导 . . . . . . . . . . . . . . . . . . . . 7205.2 Coq证明脚本生成 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7305.2.1 证明概要 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7305.2.2 初始和扩展大步 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7405.2.3 小步推导导致扩展大步推导 . . . . . . . . . . . . . . . . . . . . 7505.2.4 扩展大步推导导致小步推导 . . . . . . . . . . . . . . . . . . . . 7606 实现和评估 7806.1 实现 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7806.1.1 选项和优化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7806.1.2 Ocaml解释器 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7906.2 评估 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 800I 第一部分的结论 8307.1 相关工作 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8307.2 限制和展望 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8507.2.1 多态 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8507.2.2 匿名函数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 860II 元语言变换 8908 高阶骨架语义 9008.1 语法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9208.2 具体解释 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9409 函数对应入门 9909.1 用伪代码重写语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9909.2 CPS变换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10009.3 去功能化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10109.4 抽象机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103130目录010 骨架语义的非确定性抽象机 104010.1 伪解释器 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104010.2 CPS-变换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105010.3 去功能化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106010.4 抽象机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108010.5 认证 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109011 骨架语义的确定性抽象机 112011.1 CPS-变换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112011.2 去功能化和抽象机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114011.3 认证 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116012 认证解释器 1180II 第二部分的结论 1220结论 1260参考文献 1290IMP上的函数对应 1350A.1 语法和大步骤语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1350A.2 CPS变换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1360A.3 去功能化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1370A.4 抽象机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1390B IMP在骨架语义中的连续变换 1410B.1 初始IMP骨架语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1410B.2 添加强制转换后 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1430B.3 创建新构造函数后 . . . . . . . . . . . . . . . . . . . . . . . . . . . 1450B.4 最终的小步骤骨架语义 . . . . . . . . . . . . . . . . . . . . . . . . . 1480B.5 Coq认证的扩展大步骤 . . . . . . . . . . . . . . . . . . . . . . . 1510B.6 没有重用的结果小步骤 . . . . . . . . . . . . . . . . . . . . . . . . 1530C 证明变换 1590C.1 定义和证明结构 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1590C.2 基本引理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1630C.3 SSA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1670C.4 变换阶段的属性 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1700C.5 大步和扩展大步 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177140目录0C.6 扩展大步蕴含小步 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1780C.7 小步推导出扩展大步 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1840D NDAM和AM的完整推导 1930D.1 NDAM伪代码的连续阶段 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1930D.1.1 初始伪代码 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1930D.1.2 CPS变换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1960D.1.3 去功能化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1990D.1.4 非确定性抽象机器 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2030D.2 AM伪代码的连续阶段 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2060D.2.1 CPS变换 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2060D.2.2 去功能化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2100D.2.3 确定性抽象机器 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215150引言160第1章0引言0软件开发使用编程语言作为人类和计算机之间的沟通工具。0程序员和我们的计算机之间。这些语言的形式化定义对于防止0人类和电子设备之间的翻译问题。0语言的语法表达了哪些对象是该语言的有效程序。0程序可以被视为数学对象，并且可以用语法来描述。0语言的语义赋予了这些程序的含义，并且对于对它们进行推理是至关重要的。0根据使用情况，这个“含义”可以是一个逻辑关系，甚至是另一个数学0数学对象。在本文档中，我们仅限于操作语义，其中程序0被解释为一系列计算。即，操作语义解释了我们如何0运行程序。0形式化操作语义可能存在问题。当能够时，就像小型语言一样，0最好使用明确的推理规则。然而，对于更复杂的语言，0推理规则可能难以阅读、编写和维护。因此，语义行为是0通常以纯文本的形式陈述，具体程度不同。例如，JavaScript的语义0非常精确，可以看作是推理规则的英文翻译，而Python0文档提供了更高级的行为解释。0非正式的论文定义不适用于语言属性的认证或0算法或工具的验证。为此，最好在一个0计算机，无论是在通用的证明助手还是在专门的框架中。定理证明器是0全面的工具，不限制可表达的语义范围，但可能需要。0每种语言都需要进行校准。值得注意的例子包括JSCert [16]，一个Coq [52]。0JavaScript的语义，以及CakeML [33]，一个完全形式化的语言。0Isabelle [39]证明助手。0专门的框架可以简化形式化过程，并自动提供相关的。0工具，例如从语义生成可执行解释器。例如，Ott [50]和。0Lem [42]是一种轻量级工具，提供了一种类似于推
我的内容管理
展开
