0博士学位论文0雷恩第一大学0第601号数学与信息与通信科技学院专业：计算机科学0Adam KHAYAM0描述有效和分布式语义的元方法0论文在2022年11月30日在雷恩INRIA的Salle Métivier (C024)进行答辩研究单位：CELTIQUE/EPICURE0答辩前的评审人：0Catherine DUBOIS，教授，国家信息技术与工业计算机学院Sukyoung RYU，教授，韩国科学技术高级学院0评审委员会成员：请注意，如果在答辩当天有任何评审委员会成员缺席，评审委员会的组成必须进行调整以确保符合要求，并且必须在论文封面上进行反映0主席：Sandrine BLAZY，雷恩第一大学教授 评审人：XavierRIVAL，INRIA巴黎研究主任Arthur CHARGUÉRAUD，INRIA南锡研究主任0博士导师：Alan SCHMITT，INRIA雷恩研究中心研究主任，博士导师：Tamara REZK，INRIA SophiaAntipolis研究主任iii0致谢0又一次经历结束了，我对宇宙表示感谢。我似乎昨天才开始我的博士之路，现在它已经结束了。0首先，我要感谢仔细阅读我的论文并提出有见地评论的评审人。这是一份如此沉重的文件，所以我只能感谢你们花时间阅读和评论。同样，我要感谢评审委员会的其他成员：时间是宝贵的，把你们的时间奉献给我意义重大。0现在让我们谈谈这三年。即使在大流行期间，我在雷恩度过了美好的时光。这段时期的支柱之一就是我的团队（Celtique/Epicure）。我感谢你们每一个人，我喜欢一切，但我是小事的粉丝。例如，在大流行开始时，你们组织了“la pausecafé”每天下午聊天。这是一丝正常的闪光。我对你们非常尊重，我无法再幸运了。Celtique/Epicure团队太棒了。0特别感谢我在雷恩的朋友们。在一个疯狂的时期，我们度过了美好的时光。我们彼此是一个堡垒，我们让那场危机成为我们生活中最美好的部分之一。我想引用你们每个人和你们的论文。这是一种以物质方式个别感谢你们的方法，但突然间我意识到你们已经有太多的引用了:p。0我还要感谢我在SophiaAntipolis的同事们，我在尼斯的朋友们，以及经常从巴黎来访的人们。我总是在那里找到一个很好的环境，并受到地板上的两个团队INDES和STAMP的欢迎。0然后，让我们谈谈我在学术界的父母，先是Alan和Tamara。谢谢你们雇佣我，希望我没有让你们失望。我从你们身上学到了很多东西，我对你们对我的信任始终心存感激。Alan，这是一次相当的冒险。我作为一个外行来找你，你有耐心和能力向我介绍这个课题。你的知识和个性对我帮助很大。每当我对该做什么感到不安时，我知道我有你在背后支持我。我很幸运。我没有希望有一个更好的学术家庭。0让我们去找我的亲生家人吧。非常感谢你的耐心，尤其是当我不接电话和回复时。我爱你！0最后但并非最不重要的：Moudy，没有你就没有一切的开始。谢谢你，iv0兄弟！0标题：一种描述有效和分布式语义的元方法0关键词：Skeletal Semantics；规范语言；ECMAScript；单子；分布式0系统；分布式系统；物联网0摘要：编程语言语义的研究是计算机科学领域的一个方向，旨在形式化地表示程序的行为。在过去的四十年中，技术的进步使得提供越来越多适用于进行这些研究的框架成为可能。虽然已经存在许多已知的具有积极特征和局限性的语义风格，但在描述和研究编程语言语义方面仍有很多工作要做。本论文提出了一种方法论，旨在提供一种编写简洁且视觉上接近规范的语义的方法。为此，我们使用了一些代数构造，结合我们纯函数式的方法，得到了清晰、简洁且易于维护的形式化。我们将这种技术应用于两个案例研究，即JavaScript规范ECMAScript的建模和描述表示物联网应用行为的编排语义的形式化模型的表示。这些工作清楚地展示了我们的形式框架Skeletal Semantics [8, 41]的潜力和表达能力。本文既是对使用SkeletalSemantics的介绍，也展示了如何将其应用于编程语言，即使这些语言具有复杂且庞大的规范。同时，本文还研究了如何利用这样的工具的特性来产生清晰且可读的形式化表示。总之，本论文旨在将针对特定研究人员类别的语言的数学表示转化为对程序员构建实际实现的有价值的支持。0摘要：编程语言语义的研究和生成是计算机科学领域的一个方向，旨在形式化地表示这些对象的行为。现有技术提供了不同的风格和技术来处理语义。在过去的四十年中，技术的进步使得提供越来越多适用于进行这些研究的框架成为可能。一方面，语义风格具有众所周知的积极特征和局限性。另一方面，语义工具是一个活跃的研究课题。本论文提出了一种在名为Skel [41]的小型函数元语言中编码语义的方法论。该语言具有一套工具，用于生成不同类型的研究所需的不同工件。本论文提出的方法论展示了如何编写简洁的语义，使其在视觉上接近编程语言规范。0标题：描述有副作用和分布式语义的元方法0关键词：Skeletal Semantics；规范语言；ECMAScript；单子；分布式0系统；物联网0摘要：编程语言语义的研究和生成是计算机科学领域的一个方向，旨在形式化地表示这些对象的行为。现有技术提供了不同的风格和技术来处理语义。在过去的四十年中，技术的进步使得提供越来越多适用于进行这些研究的框架成为可能。一方面，语义风格具有众所周知的积极特征和局限性。另一方面，语义工具是一个活跃的研究课题。本论文提出了一种在名为Skel [41]的小型函数元语言中编码语义的方法论。该语言具有一套工具，用于生成不同类型的研究所需的不同工件。本论文提出的方法论展示了如何编写简洁的语义，使其在视觉上接近编程语言规范。0为了做到这一点，我们结合了不同的代数构造来编写精确、简洁、可读性强且易于维护的形式化。我们已经将这种技术应用于两个案例研究，即JavaScript规范ECMAScript的建模和描述表示物联网应用行为的编排语义的形式化模型的表示。这些工作清楚地展示了我们的形式框架Skeletal Semantics[8] 的潜力和表达能力。本文是SkeletalSemantics的介绍，展示了如何产生可用且易于阅读的不同类型规范的形式化——基于推理规则和散文。本质上，目标是将针对特定研究人员类别的语言的数学表示转化为对程序员构建实际实现的有价值的支持。0法语摘要0任何编程语言都可以被看作是一组表示其原子元素行为的规则（语义）。考虑到某些数据（输入）和编程语言的语法实例（程序），解释是一个过程，通过根据语言规则对数据进行处理来转换数据，从而返回结果（输出）。0可以将自然语言与之进行合理的类比。实际上，如果用自然语言构建可以由对话者解释的话语，那么用编程语言则可以产生程序，即机器的指令。要理解这些指令，需要一个将程序解释为机器的程序。后者必须清晰明确，因为程序的解释需要一个表示该程序所写的语法和语义的表示。0在本论文中，我们讨论了不同类型的编程语言语义和它们的表示。具体而言，我们提出了一种有效的方法来以简洁和忠实于表示其行为的规范的方式来表示编程语言的语义。这些语言可以是不同类型的，倾向于以自然语言或伪算法语言的方式非正式地定义，或者以数学符号的方式正式地定义。在本论文中，我们将展示通过一个称为Skel的小型元语言，我们能够捕捉这两种规范的语义。从这些形式化的定义中，我们然后提取代码，以便能够模块化地生成一个可以执行程序的解释器。0第七章0在骨架语义中定义语言0tique.0为了正式表示编程语言的定义，通常需要定义语言构造的语法和语义。0例如，如果我们考虑一个只进行整数加法的编程语言，我们可以如下定义其语法。0VALUE v ::= n0EXPR e ::= v | e1 + e20使用这种表示法，我们说语言的值是整数，在这种情况下，它们没有真正的定义，而语言的表达式要么是一个值，要么是两个表达式之间的和。0关于该语言中表达式的语义，有各种不同的形式可以使用。在本论文中，我们将限制在操作语义，这是一种用于描述语言构造如何执行的逻辑框架。在接下来的内容中，我们介绍上述定义的小例子的语义。0VALUE0n � e n0ADDITION e1 � n1 e2 � n20e1 + e2 � n1 + n20第一条规则，Value，如果表达式只是一个语言值，则返回一个整数。第二条规则，Addition，计算加法。对于一个和式，它计算加法的第一个项，第二个项，并返回两个整数的和。由于表达式的定义是递归的，这个简单的规则也评估了包含其他整数之间的加法的和式作为子表达式。在论文中，我们将使用骨架语义[8]来编写大部分语义。0为了立即了解骨架语义和Skel的强大之处，我们需要考虑规则的结论，n1 +n2。与整数一样，加法也没有真正的定义，除非我们自然地给出它。Skel语言是一种小型函数式语言，定义如下。0viii0用于编写语义。就像使用加法对该语言进行形式化定义一样，我们可以使用相同的抽象级别在Skel中定义该语言。该语言描述了规则，而不是表示该规则的程序。0type int type value = | Int int type expression = | Val value | Plus(expression, expression)0val plus: expression -> expression -> int0val eval (e: expression): nat =0branch let Val (Int n) = e in n or letAdd (e_1, e_2) = e in let n_1 = evale_1 in let n_2 = eval e_2 in plus n_1n_20结束0实际上，通过查看代码，我们可以看到我们定义了三种类型，一种是整数，一种是值，一种是表达式，但与后两者不同，整数类型int没有定义。加法valplus也是如此。这个操作并没有定义求和的算法，它只是表示存在一个项，它接受两个整数并返回一个整数。至于函数eval，在表达式是值的情况下，它返回封装在值中的整数，否则，对于加法，它计算第一个表达式，第二个表达式，最后返回两个整数的和。0通常，对于如此小的语言来说，在纸上或在机器上编写编程语言的语义是无关紧要的。问题出现在语言变得很大的时候。事实上，仅仅因为需要定义大量的符号才能得到紧凑的形式化，所以在纸上证明大型语义几乎是不可能的。此外，通过纸上的大型语言定义进行归纳证明也是复杂的。在过去的几十年里，已经有不同的方法达到了最先进的水平，目的是能够在计算机上编写语义，并利用计算机的支持来证明交互。0ix0结果是准备好的。有两种哲学观：一种是使用诸如Coq [70]、HOL [29]、Isabelle[30]、Twelf [71, 27]等证明助手，另一种是利用软件和为编写语义而定义的环境，如K[63]、Ott [66]、Lem [55]、PLT[36]。Skel语言属于第二类。与第二类的竞争对手不同，Skel不能直接执行程序，但可以通过necro [53]提供的工具生成各种工件。0我们将在本论文的第一部分讨论语义风格和工具。0在第2部分和第3部分中，我们将展示如何利用这种语言编写具有复杂行为的语言的语义。0贡献0博士论文的贡献在第二部分和第三部分中介绍。0在第二部分中，贡献是以一种简洁、忠实于规范、易于维护的方式描述语义，并生成一个解释器以执行程序。我们将考虑具有副作用的语言，如内存修改、异常存在和代码挂起。在本论文的这一部分中，我们首先介绍一系列玩具语言及其在Skel中的形式化。这些语言将是彼此的扩展，并且它们的形式化结构将保持相同，将副作用的传播委托给单子操作符。稍后，我们将介绍ECMAScript的机械化。我们将使用相同的方法来产生一个结构上坚实的形式化描述。在这种情况下，贡献是ECMAScript语义的简洁、可维护和可读的形式化，生成一个功能性解释器并执行小型程序。0在论文的第三部分，贡献是对已有的表示特定分布式系统行为的语义进行细化。实际上，该系统的背景是包括与网络连接的设备进行交互的Web应用程序。我们通常将这些系统称为物联网（IoT）。该部分的另一个贡献是0x0该部分的另一个贡献是为该模型定义一个调度器，限制非确定性，使模型可执行。为了支持调度器的正确性，我们将提供非确定性语义与调度器语义之间的等价定理。0论文的第二部分的贡献已经在两篇发表的文章和一篇正在修订中的文章中介绍[34, 33, 35]。0论文的第三部分的贡献目前正在以文章形式撰写。0论文的计划0论文分为三个部分。0第一部分将在第1章介绍用于形式化表示编程语言构造行为的标准技术，并在第2章介绍用于在计算机上形式化表示这些语言的软件。具体而言，最后一章将介绍骨架的语义和Skel语言，这是一种小型函数式语言，用于编写语言规范。0论文的第二部分将讨论如何捕捉语言规范的副作用。例如，语言可能会修改状态、处理异常、暂停执行某些代码段。这些副作用通常很难处理，因为它们必须在纯函数式语言中明确表示。0在第3章中，我们将展示如何逐步扩展一个小型玩具编程语言的语义，引入新的语言构造和副作用。我们将展示通过使用Monad操作符，我们将能够以极其模块化、强大和易于扩展的方式编写规范。副作用的传播将由Monad操作符隐式处理。0在第4章中，我们将使用前一章中定义的语义编写技术来表示一个真实语言JavaScript的语义。0xixii0与前一章不同，语言规范是通过逻辑推理规则描述的，而在本章中，我们将基于文本规范。与其他语言（如Python）不同，JavaScript的规范非常精确。我们将展示我们的编写技术如何准确、简洁、可维护地捕捉语言的行为。从形式化表示开始，我们将生成一个JavaScript核心解释器，并展示一个小程序的执行。能够完整表示规范是理想的，事实上，我们的主要贡献是展示语言足够表达这个历史上困难的任务相对简单。本文的第三部分将在第5章介绍代表分布式系统行为的语义。该模型旨在表达物联网环境中这些系统的演变。我们将首先通过推理规则，然后通过Skel展示语义。我们将讨论该模型的执行复杂性，该模型本质上是非确定性的，并提出一个调度器解决方案，以尝试限制该模型固有的非确定性。我们将展示调度器的语义与非确定性语义等价，从而使得无论程序的复杂性如何，都可以在该模型上执行程序。xiii0目录0引言 20I 背景 501 语义风格 701.1 While语言 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 801.2 操作语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1001.2.1 结构操作语义 . . . . . . . . . . . . . . . . . . . . . . . . . . 1101.2.2 大步操作语义 . . . . . . . . . . . . . . . . . . . . . . . . . . 1501.3 抽象机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1801.4 漂亮的大步语义 . . . . . . . . . . . . . . . . . . . . . . . . . . 2102 Skel规范语言 2702.1 Skel语言 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2802.1.1 Skel中的算术语言 . . . . . . . . . . . . . . . . . . . 2902.1.1.1 语法和语义 . . . . . . . . . . . . . . . . . . 2902.1.2 Necro生态系统 . . . . . . . . . . . . . . . . . . . . . . . 3202.1.3 算术语言的解释器 . . . . . . . . . . . . . . . . . . . 3602.2 相关规范语言 . . . . . . . . . . . . . . . . . . . . . . . 3902.3 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410II 有副作用的语义 4303 简洁描述有副作用的语义 4503.1 有副作用的算术语言 . . . . . . . . . . . . . . . . . . . . . . . . 4703.2 PCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5403.3 向PCF语言添加状态 . . . . . . . . . . . . . . . . . . . . . . 5903.4 完全的Monad骨架语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . 6403.5 显式的Continuation操作 . . . . . . . . . . . . . . . . . . . . . . . 690目录03.5.1 程序示例 . . . . . . . . . . . . . . . . . . . . . . . . . . 7003.5.2 语法和语义 . . . . . . . . . . . . . . . . . . . . . . . . 7103.5.3 带有Yield和异常的有状态PCF语言在Skel中 . . . 7703.6 相关工作 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8104 用骨架语义忠实地描述ECMAScript 8504.1 ECMAScript算法在Skel中 . . . . . . . . . . . . . . . . . . . . . . . 8704.1.1 ECMAScript . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8704.1.2 形式化的挑战 . . . . . . . . . . . . . . . . . . . . . . . . . . 8804.1.3 完成记录和ECMAScript错误处理(?!)Monad 9704.1.4 控制流Monad . . . . . . . . . . . . . . . . . . . . . . . . 10004.1.5 Skel中的一个真实示例 . . . . . . . . . . . . . . . . . . . . . . 10304.1.6 当前状态 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10604.2 解释器评估 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10904.2.1 解释器实例化 . . . . . . . . . . . . . . . . . . . . . . . 10904.2.2 评估 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11004.2.2.1 框架比较 . . . . . . . . . . . . . . . . . . 11004.2.2.2 程序执行 . . . . . . . . . . . . . . . . . . . . 11204.3 相关工作 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1130III 分布式语义 11705 可执行的分布式物联网应用语义...11905.1 背景...12105.2 WEBI：物联网应用的形式语义...12305.2.1 WEBI配置...12305.2.2 语义...12705.2.2.1 WEBI转换关系...12905.2.2.2 客户驱动规则...12905.2.2.3 服务驱动规则...13505.2.2.4 设备驱动规则...13805.2.2.5 评估函数...14205.2.3 示例：非确定性的成本...14505.2.3.1 初始WEBI配置设置...1460xiv0目录05.2.3.2 执行...15205.3 WEBI调度程序...15505.3.1 语义...15505.3.1.1 调度程序的假设...15605.3.1.2 调度配置...15905.3.1.3 小步骤语义...16105.3.2 调度程序和WEBI语义的等价性...16805.3.2.1 交换引理...16905.3.2.2 区间引理...17305.3.2.3 定理1的证明概述...17505.3.3 在Skel中执行第5.2.3节的示例...1770结论1820参考文献1870xvxvii0图表目录01.1 While语言语法的定义...801.2 表达式求值函数φ...1001.3 示例...1001.4 小步骤表达式求值。此描述与图1.2中定义的行为相匹配...1201.5 小步骤命令求值...1301.6 大步骤中的命令求值...1601.7 程序的大步骤推导树的第一层。我们在引用程序的其余部分时使用...1701.8 表达式求值的抽象机器定义...1901.9 命令求值的抽象机器定义...2001.10 使用Option结果进行大步骤的表达式求值...2201.11 Pretty-Big-Step中的表达式求值...2301.12 Pretty-Big-Step风格中语言的语法定义...2401.13 Pretty-Big-Step中的命令求值...2502.1 While构造函数的骨架...2802.2 算术语言...3002.3 Skel中的算术语言定义 . . . . . . . . . . . . . . . . . . . . . . . . . . 3102.4 Necro生态系统 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3202.5 解释monad模块及其身份monad实例化 . . . . . . . . . . . . . . . 3402.6 UNSPEC模块类型及其函数 . . . . . . . . . . . . . . . . . . . . . . . . . 3802.7 INTERPRETER模块类型及其函数 . . . . . . . . . . . . . . . . . . . . . . . 3903.1 异常类型的语法 . . . . . . . . . . . . . . . . . . . . . . . . . . 4803.2 扩展了除法和异常的算术语言规则 . . . . . . . . . . . . . . . 4803.3 扩展了除法和异常的Skel中的算术语言 . . . . . . . . . . . . . . . 4903.4 Skel中的异常monad，以及其在eval函数中的应用 . . . . 5203.5 异常monad及其在eval中的符号应用 . . . . . . . . . . . . . . . . . . 53xviii0图表目录03.6 实现零项 . . . . . . . . . . . . . . . . . . . . . . . 5403.7 PCF语义规则 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5603.8 Skel中的PCF语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . 5703.9 OCaml中的extEnv实例化 . . . . . . . . . . . . . . . . . . . . . . . . . 5803.10 带有引用的PCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6203.11 更新函数的示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . 6603.12 用于创建闭包的函数。输出是monad中的计算. 6703.13 Yield的分隔序列 . . . . . . . . . . . . . . . . . . . . . . . . . 7003.14 通过Yield进行双向通信 . . . . . . . . . . . . . . . . . . . . . . . . . 7103.15 PCF + state + delimited continuations的抽象机 . . . . . . . . . . . . . . . 7303.16 Skel中的Yield语言 . . . . . . . . . . . . . . . . . . . . . . . . . . . 7703.17 通过Yield进行Ping-Pong状态更新 . . . . . . . . . . . . . . . . . . 8104.1 Skel中的State Monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8904.2 对象 { n : 42} 的内部表示 . . . . . . . . . . . . . . . . . . . . . . . . 9604.3 算法步骤示例，需要局部环境. 9604.4 ES Completion Records的Skel形式化 . . . . . . . . . . . . . . . 9704.5 Out和Anomaly声明 . . . . . . . . . . . . . . . . . . . . . . . 9804.6 ? 和 ! 的模型 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9904.7 带有绑定器和设置器的controlFlow类型 . . . . . . . . . . . . . . . . 10004.8 带有和不带有Control Flow Monad的代码 . . . . . . . . . . . . . . . . 10104.9 带有异常的Figure 4.8的变体 . . . . . . . . . . . . . . . . . 10304.10 ECMAScript的GetValue(V)及其Skel形式化 . . . . . . . . . . . . . . . 10404.11 可产出的抽象闭包 . . . . . . . . . . . . . . . . . . . . . . . . . . 10804.12 TYPES模块实例化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10904.13 以K框架编写的GetValue 5.1 . . . . . . . . . . . . . . . . . . 11104.14 JSCert中的GetValue 5.1 . . . . . . . . . . . . . . . . . . . . . . . . . . 11204.15 JS程序示例 . . . . . . . . . . . . . . . . . . . . . . . . . . . 11305.1 ServiceInit规则。客户端初始化。该客户端的启动调用生成一个运行中的Web服务. . . .. . . . . . . . . . . . . . . . . . . 13005.2 ServiceInit Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . . 13105.3 ClientStep规则。一个Web客户端执行一个评估步骤。. . . . . . 13205.4 ClientStep Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . . 13205.5 ClientCall规则。客户端调用Web服务。. . . . . . . . . . . . . 133xix0图表目录05.6 ClientCall Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . . 13305.7 Run规则。当客户端计算完成时，它选择一个thunk并执行它。. . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . 13405.8 Run Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13505.9 ServiceStep规则。服务执行一个评估步骤。. . . . . . . 13505.10 ServerStep Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . . 13605.11 RetServiceBoot规则。与引导客户端相关的服务完成计算。它将结果返回给客户端。. . . .. . . . . . . . . . . . 13705.12 RetServiceBoot Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . 13805.13 RetService规则。与运行中客户端相关的服务完成计算。它将结果返回给客户端。. . .. . . . . . . . . . . . . . 13805.14 RetService Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . . 13905.15 DeviceSensor规则。一个传感器或一组传感器检测到一个物理事件。. . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . 13905.16 DeviceSensor Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . 14005.17 DeviceActuator规则。一个服务向设备发出执行命令。设备执行该命令。. . . . . . . . . .. . . . . . . . . . 14005.18 DeviceActuator Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . 14105.19 DeviceReading规则。一个服务向设备发出读取命令。设备响应并返回序列化的值。.. . . . . . . . . . . . 14105.20 DeviceReading Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . 14205.21 伪随机解释单子。. . . . . . . . . . . . . . . . . . . . . . . . . . 14305.22 列表解释单子。. . . . . . . . . . . . . . . . . . . . . . . . 14405.23 ServiceInit Skel规则。. . . . . . . . . . . . . . . . . . . . . . . . . . . 14505.24 windowManager服务定义。. . . . . . . . . . . . . . . . . . . . 14705.25 turnOnOven服务定义。. . . . . . . . . . . . . . . . . . . . . . 14705.26 定义调用windowManager和_I_集合的客户端。. . . . . 14805.27 定义设备的语义。. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14905.28 窗口语义。代码是用简化版本的Skel编写的，例如包含字符串。. . . . . . . . . . . . . . . . . .. . 14905.29 温度计语义和实例化。. . . . . . . . . . . . . . . . . . . . . . . . . 15005.30 世界预言机. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15105.31 一系列规则应用展示了前文中介绍的初始设置的执行过程。. . . . . . . . . . . . . . . . . . .1520图表目录05.32两个规则应用序列展示了考虑两个客户端的新设置的执行过程。第一个序列展示了一个产生有趣物理事件的交互，而第二个序列没有展示这种交互。. . . . . . . . . . . . . . . . . . . . . . . . . .. 15405.33 代表评估函数的两个图表。图表 A 描述了非确定性评估函数，图表 B描述了调度器的评估函数。 . . . . . . . . . . . . . . . . . . . . . . . . . . 15705.34 对 Π 上的过滤函数，其中 lfilter 是函数式编程中列表的经典过滤函数。 . . . . . . . . . . .. . . . . . . . . . . . 16105.35 第1步的语义规则 . . . . . . . . . . . . . . . . . . . . . . . . . . 16205.36 第2步的语义规则 . . . . . . . . . . . . . . . . . . . . . . . . . . 16305.37 第3步的语义规则 . . . . . . . . . . . . . . . . . . . . . . . . . . 16405.38 第4步的语义规则 . . . . . . . . . . . . . . . . . . . . . . . . . . 16505.39 第5步的语义规则 . . . . . . . . . . . . . . . . . . . . . . . . . . 16605.40 第6步的语义规则 . . . . . . . . . . . . . . . . . . . . . . . . . . 16705.41 第7步的语义规则 . . . . .
我的内容管理
展开
