模块演算的动态链接控制机制

理论计算机科学电子笔记138（2005）3-35www.elsevier.com/locate/entcs低优先级链接1达维德·安科纳2索尼娅·法戈齐3埃琳娜·祖卡4DISI热那亚大学Genova，意大利摘要在我们以前的工作的基础上，我们提出了一个简单的模块演算，其中模块组件的执行步骤可以与重构步骤（即，在模块级别的减少）交织，并且执行可以部分控制这些重构步骤之间的优先级。这是通过一个低优先级的链接操作符来实现的，该操作符仅在尚未链接的某个组件可用并且确实需要执行以继续进行时才执行，否则优先于外部操作符。 我们通过一些例子来说明这种机制我们通过结合静态类型系统和动态检查来确保可靠性，静态类型系统可以防止应用模块运算符时出现错误，动态检查可以在运行程序需要无法通过重新配置步骤提供的组件时引发链接错误。特别是，如果所有组件都可能可用，则不会引发链接错误。保留字： 模块演算，动态链接。1介绍传统的模块演算[6，16，13，2]基于模块操作的静态视图，在这个意义上，开放代码片段可以灵活地组合在一起，但所有模块操作只能在启动1由动态装配、重构和类型检查-欧共体项目IST-2001-33477和APPSEM II -专题网络IST-2001- 38957 i部分支持。2 电子邮件地址：davide@disi.unige.it3电子邮件地址：fagorzi@disi.unige.it4 电子邮件地址：zucca@disi.unige.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.0094D. Ancona等人/理论计算机科学电子笔记138（2005）3程序的执行，即模块组件的评估。相反，现代编程环境，如Java和C#，支持软件片段的动态链接，更一般地说，我们可以预期，在未来的系统将支持越来越多的形式的重构和标准执行步骤的交互因此，为这些功能提供基础的干净而强大的模块演算的定义是一个重要的开放问题。在以前的工作中，我们已经提供了一个例子，在这个方向上提出CMS1[4]，CMS（模块系统的微积分）[6]的扩展，其中模块运算符按需执行，也就是说，只有当执行程序否则会卡在当前配置中时。因此，配置步骤不需要总是完全执行，但是那些将要执行的步骤从开始就被唯一地确定，与程序执行无关。然而，在实践中的一个重要问题是允许用户程序动态地决定应该执行哪些配置步骤以及以何种顺序执行在本文中，我们通过定义一个新的演算CMSl，l-丰富，通过一个非常简单但相当强大的机制，从正在运行的程序中驱动配置步骤。也就是说，我们添加了一个低优先级的链接操作符，它只在某个组件（还没有被链接）可用并且确实需要执行才能继续时执行，否则优先于外部操作符。通过这种方式，可以通过适当地使用用户代码中的变量来实现对配置步骤之间的优先级的控制我们通过一些例子来说明这种机制的表达能力。值得注意的是，使用这个更懒惰的链接操作符，可以在面向对象的上下文中对现有的动态链接机制进行建模。例如，在[12]中，我们定义了一个Java动态类加载（使用多个加载器）到演算中的简单模型的编码。更一般地说，具有不同链接操作符的模型代表了一个有趣的框架，它不仅允许更好地理解现有的动态链接机制，而且还可以研究和比较它们的可能变化支持动态重构的系统中的一个关键问题是在可伸缩性和防止错误的能力（卡住减少）的相反要求之间的在我们提出的演算中，我们能够在一个简单的形式化设置中研究这个问题，其中错误要么是由于错误地应用了模块运算符，要么是由于执行需要一个当前既不可用的模块组件，也不能通过重构步骤提供虽然第一种错误应该并且可以很容易地被静态类型系统排除，但是对于D. Ancona等人/理论计算机科学电子笔记138（2005）35我KJKK需要一些成分，都被排除了。改进可以通过基于依赖的类型系统来获得，正如我们在[4]中为CMS1开发的那样，代价是增加复杂性。出于这个原因，在本文中，我们更倾向于通过将静态类型分析与动态检查相结合来探索不同的解决方案，以便更好地支持配置以多种方式演变的系统，这些方式在编译时很难预测更详细地说，也允许执行缺少某些组件的配置，可能会引起链接错误err（X：τ，π），如果运行的程序需要具有类型τ的组件X，并且没有可用的定义，由类型赋值π指定，可以通过应用给定的模块运算符与X2微积分的非正式介绍在本节中，我们通过一些例子来说明CMS1，1-及其表达能力为了简单起见，我们省略了模块组件中的类型注释，这与此无关。CMSl，l-的术语被称为配置，有两种类型：非可执行表达式或模块表达式，其与基于静态操作的传统模块演算一样，以及可执行表达式，粗略地说，其是与运行程序配对的模块表达式（底层核心语言中的表达式），使得程序执行的步骤和模块级的缩减步骤可以交错。模块表达式与CMS一样，模块表达式构建在基本模块之上，其形式为：Σxi<$→Xi∈1.. n;Yj›→ej∈1.. m;xJΣ›→eJk∈1.. p其中三个映射分别对应于模块的输入、输出和本地组件，Xi、Yj是（输入和输出）名称，用于引用来自模块外部的组件，因此在模块组成中相关，而xi，xJ是（延迟和局部）变量，用于引用组件从模块内部，因此出现在表达式ej，eJ中但不相关模块组成。输出和本地组件具有相关联的定义，其是底层核心语言（CMS1，1-，作为CMS，是一种参数演算，可以在不同的核心演算之上实例化，用于定义模块组件），而输入组件已声明但尚未定义。K6D. Ancona等人/理论计算机科学电子笔记138（2005）3例如，表示为e [x1，.，xn]具有自由变量x1，.，xn，M1=[x<$→X;Y<$→e1[x，y];y<$→e2[x，y]]是具有一个输入、一个输出和一个本地组件的基本模块使用一些语法糖，这可以写如下。模块M1是导入X作为x，导出Y =e1[x，y]，本地y= e2[x，y]结束M1组成模块的运算符有sum、reduce和link。只有当两个模块没有同名的输出组件（即没有冲突定义）时，才能执行两个模块的求和。在这种情况下，结果模块是通过将参数的组件放在一起来获得的：具有相同名称的输入组件是共享的，而连接延迟或局部变量（如果有的话）则通过α重命名来解决。例如，让我们将模表达式M3定义为M1以上和另一个基本模块M2=[y <$→Y;X<$→e3[x，y];x<$→e4[x，y]].然后，模表达式M3=M1+M2简化为[x<$→X，yJ<$$>→Y;Y<$→e1 [x，y]， X<$→e3[xJ，yJ];y<$→e2 [x，y]，xJ<$→e4 [xJ，yJ]]。reduce操作符执行组件名称的重命名，其中输入和输出名称被独立重命名输入重命名是一个映射，其域和共域分别是旧输入名称和新输入名称，而输出重命名则相反。例如5减小到X<$→X，Y<$→X，<$→Z|M3|Y1→Y，Y2→Y，[x<$→X，yJ<$$>→X，z<$<$→Z;Y1<$→e1[x，y]，Y2<$→e1 [x，y];y<$→e2 [x，y]，xJ<$→e4 [xJ，yJ]]。请注意，非内射输入重命名允许将两个输入名称合并（在示例中为X和Y合并为X），而非满射用于添加虚拟输入名称（在示例中为Z非内射输出重命名允许重复定义（在示例中，Y的定义被用作5tentat i on→Z意味着Z位于映射到Z中的映射和非映射的编码中。D. Ancona等人/理论计算机科学电子笔记138（2005）37Y1和Y2的定义），而非满射则用于删除输出分量（示例中的X在下文中，我们将使用缩写M\X来表示通过从M移除输出分量X而获得的模，即id|M|em，其中id是输入名称上的标识，em是所有输出名称，但X分别到所有输出名称链接操作符连接模块内具有相同名称的输入和输出组件，以便输入组件成为本地组件。比如说，linkX<$→X[x<$→X;X<$→e[x];]把 某 事 归 纳 为[;X<$→e[x];x<$→e[x]]。配置模块表达式可以被看作是一种配置语言，因为它们模拟了软件片段可以组合在一起的不同方式然而，最终我们希望获得可执行代码并运行它。这是通过选择模块组件来建模的。在传统的模演算中，如CMS，选择运算符，表示为M.X，只能在M是一个没有输入组件的基本模块时执行（所有配置步骤都已执行，并且模块是自包含的）。比如说，[;X<$→x+y;x<$→2， y<$→3].X约简为2+3，而y约简为5，其中[y<$→Y;X<$→x+y;x<$→2].由类型系统通风即使X的定义表达式不依赖于任何延迟变量，我们也会得到一个卡住的模块表达式[y<$→Y;X<$→x+3;x<$→2].注意，以这种方式，在选择之后，封闭模块结构消失，因此不可能进行配置步骤。在这里，我们希望允许模块组件的评估和重构步骤之间的交错因此，我们对选择采取了一种相当不同的观点。首先，对基本模块的选择不仅返回定义所选组件的核心表达式，而且返回基本可执行配置，即由基本模块本身和核心表达式组成的一对。 这对在组件上下文中运行的应用程序进行建模我也不想让你去。对于一个实例，[;X<$→x+y;x<$→2，y<$→3]。到再到<[;X<$→x+y;x<$→2， y<$→3]，x+y>，<[;X<$→x+y;x<$→2， y<$→3]，2 +y>，8D. Ancona等人/理论计算机科学电子笔记138（2005）3这个简单的改变允许在选择之后执行进一步的配置步骤，如下所示此外，即使仍有输入组件，也可以执行选择，因为这些缺失的组件可能永远不需要，也可能稍后通过执行配置步骤而可用。第一种情况的一个例子是由以下减少步骤所示[y<$→Y;X<$→x+3;x<$→2].X）<[y<$→Y;X<$→x+3;x<$→2]，x+ 3>）<[y<$→Y;X<$→x+3;x<$→2]，2 + 3>）<[y<$→Y;X<$→x+3;x<$→2]，5>.第二种情况的示例如下所示链接Y<$→Y（[y<$→Y;X<$→x+y;x<$→2].X+[;Y<$→3;]））链接Y<$→Y（[y<$→Y;X<$→x+y;x<$→2]，x+y>+[;Y<$→3;]））链接Y<$→Y（[y<$→Y;X<$→x+y;x<$→2]，2 +y>+[;Y<$→3;]））链接Y<$→Y[y<$→Y;X<$→x+y，Y<$→3;x<$→2]，2 +y>）<[;X<$→x+y，Y<$→3;x<$→2， y<$→3]，2 +y>）<[;X<$→x+y，Y<$→3;x<$→2， y<$→3]，2 + 3>）<[;X<$→x+y，Y<$→3;x<$→2， y<$→3]，5>。这个例子还说明了CMS1，1-的另一个特性：模块运算符我们上面描述的也可以应用于基本的可执行配置之上，给出可执行配置6;然而，在这种情况下，运算符具有懒惰行为，在这个意义上，它们是按需执行的，只有当程序执行被卡住时，因为它需要延迟变量。例如，在上面的例子中，如果X的定义是x+ 3（和前面一样），那么求和和连接运算符将不会被执行。换句话说，可执行配置的演变包括程序执行（在核心级别应用归约规则，可以管理基本模块所操作的局部变量），除非此执行需要访问当前为输入组件的模块组件。在这种情况下，必须执行重新配置步骤，直到该输入组件可用，即从另一个模块导入。然而，请注意，到目前为止，只允许有限形式的动态重构，因为所有重构步骤都是静态计划的：它们实际执行的事实取决于程序执行，但6然而，只有当最多一个（通常是左）参数可执行时，才允许使用sum，因为我们不想在这里处理多线程。D. Ancona等人/理论计算机科学电子笔记138（2005）39X›→XY→WX›→XX›→ X，Y›→W）链接不可能根据执行情况执行不同的重构步骤为了添加一种简单形式的执行驱动的重新配置，CMS1，1-还包括链接操作符的变体链接，称为低优先级链接，只能应用于可执行的配置。低优先级链路是偶数更懒惰的链接形式，其仅在程序执行否则将被卡住时执行，如其它操作符，并且此外，执行该操作符实际上将使执行的继续成为可能。这意味着在低优先级链接中指定的映射中，存在从输入名称到输出名称的关联，该关联是可执行的（也就是说，这两个名称都存在于模块中），并且其应用程序实际上允许程序继续执行（也就是说，程序恰好需要该输入组件）。在这种情况下，链接是递增执行的，也就是说，只解析所需的组件例如在linkY<$$>→Y，（link-X<$$>→X，（[x<$→X，y<$→Y;X<$→2;]，x+ 1>+[;Y<$→2;]）），Z›→ZY›→W由于执行需要组件X，链接-运算符被执行，配置一步到位，linkY<$→Y，Z<$→Z（link-< [y<$→Y;X<$→2;x<$→2]，x+ 1>+[;Y<$→2;]）。然而，如果执行需要组件Y，例如，在linkY<$$>→Y，（link-X<$$>→X，（[x<$→X，y<$→Y;X<$→2;]，y+ 1>+[;Y<$→2;]）），Z›→ZY›→W则不执行链接-，并且外部操作符被移动到内部，执行，如下所示。）linkY<$→Y，Z<$→Z（link-<[x<$→X，y<$→Y;X<$→2，Y<$→2;]，y+ 1>）--一种X›→ X，Y›→W）链接-（链接Y<$→Y，Z<$→Z[x<$→X，y<$→Y;X<$→2，Y<$→2;]，y+ 1>）<[x<$→X;X<$→2， Y<$→2;y<$→2]，y+ 1>）...X›→X，Y›→W请注意，我们考虑一种稍微自由的链接形式w.r.t. CMS和CMS1，允许对基本模块中不存在的输入名称进行关联（例如Z→Z ）：这些操作被简单地忽略。 另一方面，从当前输入名称到或者是丢失了或者是有错误的类型被卡住了（并且将被类型系统阻止）。相反，对于低优先级链路，我们还允许丢失或具有错误的输出名称的关联（例如Y→W）：执行这些链接将被推迟，直到两个名字将出现，10D. Ancona等人/理论计算机科学电子笔记138（2005）3相同的类型（由于执行了一些重构操作符）。D. Ancona等人/理论计算机科学电子笔记138（2005）311我i∈1.. ni∈1..n12-此外，在低优先级链路中，仅执行当前需要的关联。表现力我们现在展示一些稍微复杂的例子，说明低优先级链接所带来的简单机制如何强大到足以模拟各种现实世界的情况。例2.1这种配置模拟了一种情况，程序可以决定是否链接任何组件，仅链接组件X1或仅链接组件X2：-X2›→X2）.-X1›→X1）（<[x1<$→X1，x2<$→X2;z<$→ez[xi]，x0<$→e0]，e[z， . . . ]>+[. . . ;X1<$→e1，X2<$→e2;. . . ]该决定被编码在控制变量z的定义中，z又指xi，其中i∈ {0， 1， 2}：如果i=0，则没有新的分量被链接;如果i= 1（分别为i= 2），则只有分量X1（分别为X2）是有联系的例2.2本例使用软件组件库X i，i ∈ 1. N，对于该系统存在两个版本E i、EJ，例如相同的所需功能的不同实现。在第一阶段，如果程序需要某个组件Xi，则采用初始版本ei。例如，程序对前m个分量使用初始版本，其中1≤m n。然后，程序可以请求以下组件通过控制变量z链接新版本，如图所示下面在这里和下面的例子中，我们假设e [x1，.，xn]是核心表达式，其执行需要变量x1，.，xn，以此顺序。Z›→Z（链接-i∈1..（<Σ Σz→Z，xi→X;Xi→e;，Xi›→ Xiiie [x，.，x m，z，x m+1，...，x n]>）\X i∈1..n<$X<$→eJi∈1.. n， Z<$→e;i+;iiZ）例2.3在这个类似的例子中（X-2›→X201-02-X›→X（[x<$→X，x1<$→X1，x2<$$>→X2;X<$→e0;z<$→ez[xi]，x0<$→e0]，e[z，x]>）\X+[;X<$→e1，X1<$→eJ;]）\X+[;X<$→e2，X2<$→eJ;]），链路（链接链路链路12D. Ancona等人/理论计算机科学电子笔记138（2005）3该程序使用一个内部由x表示的组件，对于该组件存在三个版本：当前执行上下文中的e0和外部模块中的e1、e2关于使用哪个版本的决定被编码在控制变量z的定义中，z又引用另一个控制变量xi。如果i= 0，则使用当前版本e0;如果i= 1（分别为i= 2），则使用第一个（分别为i =2）提供的X版本。二是外部模块联动。3语法和语义符号我们写f：A→B来表示f是一个具有域A的映射，记为dom（f）和codomainB，写作cod（f）。我们将在地图上使用以下操作符• f，g是两个定义域不相交的映射的并.• f∈g是两个相容映射的并，即s. t. f（x）=g（x）对于所有x∈dom（f）∈dom（g）.• F|C是映射f：A → B到集合C的限制（即，f |C（x）= f（x），其中x∈A<$C）。• f\C是集合C从映射f：A→B的移除（即，（f\C）（x）=f（x），x∈A\C）。• f∈g表示两个映射s.t.鳕鱼（g）鱼体（f）。• fg表示映射包含（即通常的子图关系）。图中给出了演算的语法1.一、我们假设一个无限集合名称X的名称，变量x的无限集合Var，以及（核心）表达式的集合Exp（用于定义模块的底层语言的表达式组件）。 实际上，作为CMS和CMS1，CMS1，1-是参数演算，其可以在满足后续中指定的某些（标准）假设的不同核心演算上被实例化。然而，在CMS1，1-中，在CMS中，模块组件不能是模块。演算的术语是可执行的配置（简称配置）或不可执行的配置（模块表达式）。一个可执行的配置可以从一个可执行的基本配置开始，或者从一个不可执行的配置（模块表达式）M的一个组件的选择开始，并通过应用重构操作符（与模块表达式求和，归约，链接和低优先级链接）来构建。一个可执行的基本配置是一对[i;o;p]，e >，由一个基本模块和一个核心表达式组成。，其中dom（i）dom（ρ） =可执行配置可执行基本配置|C+M总和|σ ι|C| σ o约简||链接σClink-C，其中hσ=/k链路低优先级链路|M.X选择M∈Mod：：=不可执行配置|[i;o;p]，其中dom（i）dom（ρ） =不可执行的基本配置|M+M总和|σ ι|M|σ o约简|链接σM链路14D. Ancona等人/理论计算机科学电子笔记138（2005）3产品名称111222121212M ∈MCtx：：=Q|M+M|[i;o;p] +M|linkσM|σι|M|σoR M）M（M-ctx）M[RM] ）M[M]（M-sum）[i;o;p]+ [i;o;p]）[i，i;o，o;p，p]如果dom（i1，p1）<$FV（[i2;o2;p2]）=dom（i2，p2）<$FV（[i1;o1;p1]）=<$dom（i1，p1）dom（i2，p2）=dom（i 2，p 2）dom（o1）dom（o2）=dom（隐式）X：τ1∈cod（ι1）<$X：τ2∈cod（ι2）<$τ1=τ2（隐式）（M-reduct）ι|[i，IJ;o;p]|O ）[σιι，ιJ;oσo;ρ]如果 cod（iJName）dom（σi）=domcod（iName）隐藏域（σi）（隐式）cod（σo）dom（o）（隐式）X1：τ 1∈cod（i）<$σi（X 1）=X 2<$X 2：τ 2∈cod（iJ）<$τ 1=τ 2（隐式）（M-link）hihi林克σ x<$→X：τi，ι;o;ρ ）的方式i;o;p，xiii∈I i∈IExp（σ（X））如果cod（iName）dom（σ）=dom{X i |i∈I}dom（σ）（隐式）{σ（Xi）|i∈I}dom（o）（隐式）图二. 模块表达式基本（可执行和不可执行）配置只有在延迟变量和局部变量的集合不相交时才是良构的。注意，对于低优先级的链接操作符，我们要求重命名σ不为空。实际上，该运算符是按需执行的，也就是说，当运行需要X时，在σ中执行一个从X→Y的自适应运算程序（并且Y可用于正确的类型），因此指定空重命名毫无意义。我们将在介绍归约规则时更详细地解释模运算符核心语言的表达式没有指定;我们只假设它们包含变量。在非可执行配置上的sum，link和reduce的归约规则，如图所示2，完全一样，在CMS和CMS1（除了类型的装饰处理），因此，他们的解释，我们参考的例子，前一节和[6，4]的更多细节。为了清楚起见，我们还写了一些附加条件（标记为“隐式”），这些条件是多余的我›→o我D. Ancona等人/理论计算机科学电子笔记138（2005）315σσ）e eσ）的方式C∈CCtx：：=Q|C+M|linkσC|σι|C|σo|林克-CCM∈CMCtx：：=M。X|CM+M|linkσCM|σι|CM|σo|link-CME ∈ ECtx：：= Q|. . . ...这是什么？语境封闭RC）CR M）M（C-ctx）C[RC]C[C]（CM-ctx）CM[RM]）CM[M]选择规则（sel）[i;o;p].X ）<[i; o; ρ]，o（X）>X∈dom（o）（隐式）程序评价规则J核心（核心）<[i;o;p]，e>[i;o;p]，eJ>（var）<[i;o; p]，E[x]>）<[i;o; ρ]，E{ρ（x）}>x∈dom（ρ）（隐式）x/∈HB（E）错误规则（var/err）<[i; o; p]，E [x]>）err（X：τ，π）x/∈HB（E）X：τ=i（x）π=o类型(link-/err）C ）err（X：τ，π）link-C）err（X：τ，π）X/∈dom（σ）<$σ（X）/∈dom（π）<$π（σ（X））/=τ图3.第三章。可执行配置的归约规则I在规则（M-ctx）中，元变量RM的范围覆盖模块赎回，即图2中模块表达式的其他规则的左侧。我们把M[M]写成表达式M，它是通过语法上用表达式M替换M中的洞而得到的（没有任何变量重命名）。在规则（M-sum）中，FV（M）表示M中自由变量的集合，分别以明显的方式定义。在规则（M-约简）中，若σ=Xh∈HY ， Yk∈K且i=xi∈IX：τ，其中h›→ h k i›→ i iIH，然后σi=xi∈IY ：τ，xk∈KY ：τ，其中对于所有k∈K，x是名称i›→ii k›→k k k一个新变量，τk是任意类型。图3和图4.给出了可执行配置的归约规则直觉是，配置的执行开始于对在其中运行的程序的评估，可能通过从模块表达式中选择组件（图3中的规则（sel））来获得，并且该评估通过标准执行步骤进行，可能访问由基本模块（图3中的程序评估规则）所3）直到一个延迟的变量-16D. Ancona等人/理论计算机科学电子笔记138（2005）3able;在这种情况下，需要重新配置步骤（图3中的错误规则），并执行这些步骤（图4中的重新配置规则），直到变量成为局部变量，并且可以应用规则（var）上下文闭包规则有两种求值上下文，相应地，可执行配置有两种上下文闭包规则：C是一个有洞的上下文，要求C∈Conf，s. t。C[C]∈Conf，而CM是一个有洞的上下文，要求M∈Mod，s.t.CM[M] ∈Conf.在规则（C-ctx）中，元变量RC的范围超过配置赎回，是，图中其他配置规则的左手边3和图四、选择规则Rule（sel）采用不可执行的基本配置[i;o;p]，并通过选择核心表达式o（X）作为程序来使其可执行程序评价规则规则（核心）对执行步骤进行建模，该执行步骤是在基本的可执行配置中的核心表达式（我们用核心演算的归约关系表示）的方式核心规则（var）模拟了核心评估表达的情况-Sion需要一个在当前基本模块中有相应定义的变量在这种情况下，计算可以通过简单地将变量替换为其定义表达式来进行。我们用E表示核心评价上下文，并通过HB与每个核心评价关联的功能评估上下文是指围绕其孔的一组粘合剂，以明显的方式定义在这里和下面的规则中，边条件x/∈ HB（E）表示这样一个事实，即变量x在核心上下文E的洞所表示的位置上的出现是自由的（即，不被洞周围的任何绑定器捕获）。最后，我们用E{e}表示捕获，避免了上下文E的洞的替换，表达式为e。错误规则规则（var/err）模拟了核心表达式的评估需要一个变量的情况，该变量在当前基本模块中没有相应的定义在这种情况下，通过提高错误err（X：τ，π）来触发重新配置步骤，该错误err（X：τ，π）可以由外部运算符捕获，如关于重新配置规则的段落中所述。的D. Ancona等人/理论计算机科学电子笔记138（2005）317∅规则（link-/err）处理无法执行link-运算符的情况，因为没有为继续计算所需的名称X指定链接（侧条件X/∈dom（σ）），或者所需的定义缺少（σ（X）/∈dom（π））或没有适当的类型（π（σ（X））τ）。在这种情况下，误差err（X：τ，π）被传播到外部运算符（如果任何），因此要么X最终将与适当的类型τ相关联，要么整个计算将以关联误差err（X：τ，π）终止。值得注意的是，错误不会被上下文闭包规则传播;因此，它们会被周围的上下文捕获，包括通常的模块操作符（参见下面的规则（sum/basic），（sum-closure），（reduce/basic）和（link/basic））;而低优先级的链接如果不能解决错误，则会传播错误因此，直观地说，C）err（X：τ，π）成立当且仅当C中的程序求值需要一个名为X和类型为τ的输入组件，并且当前可用的输出组件是由类型赋值π指定的组件。在X的低优先级链路应用于C的情况下，使用后一信息来决定规则（link-）还是（link-/err）适用。重组规则求和、归约和连接运算符是按需执行的，只要它们所包含的配置表达式的求值需要一个延迟变量（因此，产生了err（X：τ，π每个运算符需要两种不同的规则。当封闭的配置是基本配置时，应用前者，在这种情况下，运算符在基本配置内的模块表达式上执行请注意，在基本配置中，模块操作符对模块的影响与图2所示完全相同;所有隐式副条件（为简洁起见，这里没有报告）仍然成立。后者是当封闭的配置有（当然不需要或不适用）链接-作为外部操作符;在这种情况下，操作符与链接-交换。通过反复应用这一规则，运算符进入内部，直到它可以由相应的（/基本）规则执行在rule（link-）中，只有在需要输入名称X可以安全地链接到具有适当类型的输出组件（边条件π（Y）=τ）。请注意，链接-是递增应用的，在这个意义上，只有所需的输入名称将被链接。为此，link-的应用程序被拆分为link-和link应用程序。然后，通过重复应用（link/link-）规则，操作符链接将进入任何内部链接操作符，直到它可以由（link/basic）规则执行在这个规则中，我们假设将链接-C与C标识（当完全连接时，链接-18D. Ancona等人/理论计算机科学电子笔记138（2005）3σ产品名称›→oσσ111222121212我重组规则<[i1;o1;p1]，e >）err（X：τ，π）（sum/basic）[i;o;p]，e>+[i;o;p]）[i，i;o，o;p，p]，e ><<如果dom（i1，p1）<$FV（[i2;o2;p2]）=dom（i2，p2）<$FV（[i1;o1;p1]）=<$< [i; o; p]，e >）err（X：τ，π） M）MJ（sum-closure）(sum/link-）< [i;o; p]，e >+ M ）<[i;o; p]，e >+ M Jlink-C ）err（X：τ，π）link-C+M）link-（C+M）σ σ< [i，IJ; o; p]，e >）err（X：τ，π）（reduct/basic）ι|<[i，IJ;o;p]，e>|O ）<[σιηι，ιJ;oησo;ρ]，e>如果 cod（iJName）dom（σi）=domlink-C ）err（X：τ，π）（reduce/link-）σσι|林克-C|σo ）Link-（σi|C|σo）(link/基本）σH）err（X：τ，π）hiif链接σ< xi<$∈I→X：τi，i;o;ρ，e > ）的方式cod（iName）dom（σ）=domlink-'C）err（X：τ，π）（link/link-）`σ ′linkσlink-'C ）link-'（linkσC）（link-）链路C ）err（X：τ，π）C ）link-（linkπ（Y）=τC）、σ，X<$→YσX<$→Y图四、可执行配置的归约规则2当σ = σ时，即执行）。最后，对于求和运算符，我们还需要一个进一步的规则来强制在需要时对求和的第二个参数中的模表达式求值。4类型系统根据前一节给出的归约规则，卡住的归约要么是由于错误地应用了模块运算符，就像CMS7中已经存在的那样，要么是由于程序执行需要一个当前既不我我-D. Ancona等人/理论计算机科学电子笔记138（2005）319可用，也不能通过重构步骤提供的模块组件7也就是说，不兼容的输入或在求和中连接输出组件，重命名缺少的输出名称，并链接到缺少的输出组件。20D. Ancona等人/理论计算机科学电子笔记138（2005）3σσ第一种错误可以很容易地被一个类似于[6]中最初为CMS设计的静态类型系统排除，其中模块类型是一对签名，指定输入和输出组件及其类型（对于配置，添加运行程序的类型就足够了的唯一的新颖性是低优先级链路运营商。很容易看出，该操作符不会引入任何新的键入错误，因为可以安全地应用link-不管参数C的类型如何（实际上，如果它不适用，它就没有效果）。另一方面，不太清楚结果配置的类型应该是什么：实际上，由于输入组件（比如X）的适用低优先级链接要么被执行，要么被忽略，这取决于如果运行的程序需要X，那么link-C可以有通过连接X获得的类型（即，通过删除X），或者与C相同的类型。然而，只有后一种解决方案（由图中的形式规则（C-链接-）所7）是安全的，因为从类型中删除输入名称不会引入模块的类型不安全应用程序运算符，反之则不成立（例如，我们可能最终得到一个类型不安全的和，涉及不兼容的输入组件）。为了避免“缺少组件”错误，可以由这个静态类型系统强制执行的一个简单解决方案是只考虑那些“封闭”的配置事实上，这直观地意味着，无论运行的程序需要哪个组件，这个组件最终都可以通过重新配置而变得可用然而，该解决方案具有这样的缺点，即排除了许多安全的减少，这些减少从不需要不可用的组件改进可以通过基于依赖关系的更复杂的类型系统来获得，正如我们在[4]中为CMS1开发的那样然而，在本文中，我们更倾向于探索一种不同的解决方案，因为通过引入低优先级链接操作符所获得的表达能力将由于采用过于严格的类型规则而部分丧失实际上，如上所述，在实践中，当计算术语的类型时，不考虑该运算符，而在运行时，其应用程序可以提供所需的组件。因此，我们更倾向于将静态类型分析与动态检查相结合，以防止由于缺少组件而导致的执行更详细地说，具有输入组件的配置也被认为是类型安全的，并且在运行程序需要具有类型τ的组件X并且没有由类型分配π指定的可用定义可以关联的情况下，执行可以引发链接错误err（X：τ，π）通过应用给定的模运算符，我们现在给出类型系统的形式定义模类型有f∈[πι;πo]，其中eπι，πo是符号，thatis，序列sXi：τii∈ID. Ancona等人/理论计算机科学电子笔记138（2005）321我► πι►πo{核心τi|i∈ I}► [πι;πo]► Xi ：τi∈I<$h，k∈I.Xh=Xk<$τh=τk图五. 良构模块类型ˆ► Xi：τ ii∈I;Xj：τj j∈Oxh：τhh∈ I L¯► coree k：τ k|k∈O<$L（M-基本）Hi∈Ij∈O我l∈ Li∈Ij∈O►M Xi ›→Xi：τi;Xj <$→ej：τj;xl<$→el：Xi：τi;Xj：τjMM1：[πι1;πo1]o o（M-总和）► MM1 +M2 ：[πι1ππι2;πo1πo]π1► MM：[πι;π〇]σι|dom（πι）：πι|dom（σ）→πι（M-还原） ►ι|M|o：[πιπι\d om（σi）;πιo] oooM σ σσ：ππ→π（M-link）► MM：[πι;π〇]► MlinkσM：[πι\dom（σ）;πo] σ|dom（πι）：πι|dom（σ）→πo见图6。 模块表达式由组件名称和类型组成的对。在下文中，我们将识别表示相同对集合的所有签名（即，或-D.E. D.当然了，如果有一个人Xi：τii∈I;Xj：τjj∈J，then{Xi|i∈I}和{Xj|j∈J}表示这些集合M的输入和输出分量 类型注释Xi：τi表示输入（相应地，输出）分量Xi可以正确地绑定到（相应地，与）类型τi的表达式相关联。如果两个签名πι和πo是从组件名称到格式良好的类型的两个映射，则模块类型是格式良好的 这是通过F i g中的规则s定义的judgment[πι;πo]来形式化的。5，其中re_e_c_r_r_t是在核心层上对良构类型的判断下面我们将在（格式良好的）签名上使用映射的运算符格式良好的签名）。图6和图7给出了微积分的类型系统。7 .第一次会议。模块表达式的类型判断具有形式MM：[πι;πo]，这意味着M是类型为[πι;πo]的格式良好的模块表达式。模块表达式的类型规则以与标准模块演算略有不同的形式给出[6]。实际上，除了处理类型修饰之外，它们还允许应用更一般的reduce和link操作符。在规则e（M-b）中，we表示yr∈cre：τ是core表达式的类型判断，意味着e是r中的类型τ的良构表达式，其中Γ是一个（核心）上下文，也就是说，从变量到格式良好的（核心）类型的映射请注意，模块类型必须是格式良好的。（M-sum）类型规则允许共享具有2ˆ22D. Ancona等人/理论计算机科学电子笔记138（2005）3σ相同的名称和类型，而边条件阻止输出组件共享。回想一下，表达式fg表示两个相容映射f和g的并集。因此，它隐含地认为，签名格式良好。在规则（M-reduce）和（M-link）中，具有形式σ：π1→π2的边条件确保了重命名σ保持类型;形式上，这意味着σ：dom（π1）→dom（π2）和σ（X）=Y<$π1（X）=π2（Y）。在规则（M-约简）中，与原始公式[6]不同，输