名义类型的主流面向对象编程语言的结构与继承分析

可在www.sciencedirect.com在线获取理论计算机科学电子笔记301（2014）3-19www.elsevier.com/locate/entcs一种名类型面向对象程序设计的域理论模型莫兹河AbdelGawad1美国德克萨斯州休斯敦莱斯大学计算机科学系摘要大多数当代主流面向对象（OO）软件都是使用名义类型的OO编程语言编写的。现存的面向对象程序设计领域理论模型是为了分析面向对象类型系统而开发的，它们忽略了这些主流面向对象语言的关键特性，比如名词性。本文总结了NOOP作为OOP领域理论模型的构建，它包含了在名义类型的主流OO软件中发现的名义信息。包含名义类型信息并断言静态类型OO编程语言中的类型继承是一个固有的名义概念，可以很容易地证明继承和子类型在这些语言中是完全确定的。这个结论是与使用这些语言的OO开发人员的直觉完全一致，并且与“继承不是子类型化”的信念相反因此，NOOP为分析和发展名义类型的主流OO编程语言提供了更坚实的语义基础。关键词：面向对象编程，指称语义，命名类型系统，结构类型系统，NOOP，类型名，继承，子类型，OOP，Java，C#1介绍为了发展和改进主流面向对象编程语言的类型系统，如Java [18]，C#[1]，C++[2]，Scala [24]和其他使用类名信息定义对象类型和OO子类型的语言，需要这些语言的精确数学模型。名义类型OOP的精确模型允许对这些主流OO编程语言进行精确的推理和分析另一方面，不精确的模型会导致不准确的结论。在基于类的OO语言中，对象与其类名及其超类的类名相关联，作为对象含义的一部分类1 电子邮件地址：moez@cs.rice.eduhttp://dx.doi.org/10.1016/j.entcs.2014.01.0021571-0661 © 2014 Elsevier B. V.在CC BY-NC-ND许可下开放访问。4M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3名称又与类契约相关联。2在基于类的OOP中，两个具有相同结构但具有不同类名信息的对象是不同对象。这两个对象内部的不同类名信息意味着这两个对象可以维护不同的类契约，因此这两个对象可以有不同的行为。因此，这两个对象可以被认为在语义上是不平等的。此外，在名义类型的基于类的OO语言中，类型和子类型关系利用类名和类之间的显式指定的类型继承关系，两个类的实例不在类继承层次结构中，不能相互替换（即，，不是尽管其明确的语义重要性，类名称信息（以下简称为缺少主流面向对象语言的名词性信息的面向对象程序设计模型是面向对象程序设计的结构模型，而不是名词性模型。OOP的结构模型已经导致PL研究人员对OOP做出了一些与大多数主流OO开发人员的直觉相矛盾的结论。例如，（类型）继承的协议，在句法（即，程序代码）级别，以及在语义（即，（程序意义）层次的概念是使用名义类型OO语言的OO开发人员的基本直觉。然而，现存的OOP指称模型导致了“继承不是子类型化”的不准确结论在基于类的主流OO语言中，继承是一个固有的名义概念，这是由于类名与继承的类契约的非正式关联。因此，基于OOP结构化观点的继承结论与大多数主流观点的直觉之间存在差异。OO开发人员，他们采用OOP的名义观点。这种差异促使考虑在OOP的数学模型中包含名义信息。本文介绍了一个包含主流面向对象程序设计语言名义信息的面向对象程序设计模型NOOP的构造。第一次出现在[5]。拥有一个包含名义类型化OOP的名义信息的OOP模型，应该能够在当前和未来主流OO语言的类型系统设计中取得进展 这些语言的类型系统的一些特征（例如，，泛型）似乎关键地依赖于名义信息。为了扩展语言或设计包含它们的新语言，准确地理解和分析这些特征已经被证明是困难的，当使用OOP的操作模型或使用缺乏在名义类型OO语言中找到的完整名义信息的OOP的表示模型时如[6]所示，拥有面向对象程序设计的名词域理论模型应该可以更容易和更准确地分析这些依赖于名词信息的语言的特征。从OO软件的角度来看-2类契约通常在代码文档中非正式地表达。类契约因此（直接）编码在类名中。M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）35软件开发，拥有更好的主流OO语言应该会带来更高的生产力和更高质量的代码。本文的组织结构如下。第二节简要介绍了与本文相关的研究成果。第3节然后开始正式介绍NOOP通过提出一个新的记录域构造器，称为第4节介绍了类签名和其他相关的签名构造，它们是用于体现名义类型化OOP中的名义信息的语法构造第5节介绍了NOOP的构造，使用“rec”和签名构造，然后给出了命名类型OOP中继承和子类型识别的证明。第6节介绍了我们在开发NOOP的基础上得出的主要结论。第7节通过提出可以基于NOOP开发的进一步研究来结束本文。2相关研究NOOP是名义类型OOP的指称模型。达纳·斯科特（Dana Scott）与戈登·普洛特金（Gordon Plotkin）等人一起发明并发展了域理论和指称语义学（例如，参见[29，32，30，25，12，19，16]）。指称语义的发展是通过研究Lisp [21，22]和ML [17，23]等函数式编程语言随后对面向对象程序设计的语义进行了研究。Luca Cardelli建立了第一个广为人知的OOP指称模型[9，10]。CardelliWilliam Cook和他的同事在Cardelli的工作基础上3后来，Kim Bruce [8]和Anthony Simons [31]推广了Cardelli和CookMartin Abadi和Luca Cardelli后来提出了OOP的操作模型[3，4]。这些模型也有OOP的结构视图。具有OOP的名义视图的操作模型后来得到了发展。在他们的开创性工作中，Atsushi Igarashi，Benjamin Pierce和Philip Wadler提出了FeatherweightJava [20]（FJ）作为名义类型OO语言的操作模型。尽管FJ不是名义类型OOP的第一个操作模型，但它是名义类型OO语言（即Java）最广为人知的操作模型（一个微小的核心子集）。值得一提的是，NOOP作为一个更基础的领域理论模型，命名类型的OO语言（包括Java）-为Featherweight Java中包含的命名信息其他研究类似于这里介绍的，但有不同的研究兴趣和目标，是Reus和Streicher[27，28，26]。在[26]中，开发了基于类的OOP的无类型指称模型。在这项工作中，类型信息在很大程度上被忽略了（对象方法和字段没有类型签名），一些名义信息仅包含在对象中以分析OO动态分派。[26]的模型是为了分析突变和命令而开发的[3]对Cardelli和Cook工作的详细讨论6M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3LDR LDDDD±D阿罗勒L面向对象语言的特性，用于开发面向对象软件的规范及其属性的验证。分析结构类型化和名义类型化的OO类型系统之间的区别并不是Reus和Streicher研究的目标3“Rec”（），一个新的记录域构造器为了构造NOOP，我们引入了一个新的域构造器。除了NOOP包括主流OOP的名义信息之外，NOOP模型记录为标记的有限函数而不是无限函数，这是对现存OOP领域理论模型的另一个改进（特别是Cardelli [9，10]和其他直接构建在其上的模型由于对象的形状是有限的（对象的形状是其字段和方法的名称/标签的集合），并且由于当标签被公式化为计算域的成员时，标签域的不确定性，在NOOP中建模对象促使定义一个新的域构造器，它类似于传统的功能域构造器，但有些不同。这个域构造函数，称为记录函数是显式有限的数学对象。使用构造的域是记录函数的域，该记录函数对具有从标签的随机域到值的任意域的标签的记录进行下面我们介绍记录域构造函数，然后我们讨论它的数学性质。的定义利用了基本域理论的标准定义（这些定义的总结见[5]的附录A）。3.1记录功能一个记录可以被看作是从一组标签（作为成员名）到字段或方法的有限映射。因此，我们使用显式有限记录函数对记录进行记录函数是一个有限函数，它与一个表示函数输入域的标记配对。对记录进行建模的记录函数的标记表示记录的标签集。与物体形状的定义一致，我们同样把记录的标号集称为记录的形状。因此，记录函数的标记告诉记录的形状3.2定义设是包含所有记录标签的可计算域加上一个额外的不适当的底部标签，，这使得是一个域（所有计算域必须有一个底部元素）。设是一个任意区域，具有逼近序和底元.域包含记录成员映射到的值。令表示子域关系（见[12]中的定义6.2如果我们让LfM.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）37LLDL → DRU萨尔河D±RR和|关于我们|{⊥}在L的任意有限子域上的范围（所有子域Lf包含L f），那么我们定义域R= LD为从L到D的记录函数的域，其中，|R|域R的定义为：（一）|= {R }|={⊥R}∪Lf LR（Lf，D）其中集合R（Lf，D）定义为（2）R（Lf，D）={ta g（|Lf|\{L}）} ×|Lf→D|并且其中tag是映射对应于域的形状的函数F到可计数的标签集合中的唯一标签（其确切格式不需要），并在F是 严格连续函数的定义域从F到记录函数中需要标记来确保记录域构造函数是一个连续的、实际上可计算的域构造函数。到如图所示，记录r={l1<$→d1，···，lk dk}由记录函数建模r=（tag（{l1，...，l k}），{（lL，d k），（l1，d1），...，（l k，d k）}）。应该注意的是，允许构造（唯一的）记录函数（tag（{}），{（ L，D）}），该函数对空记录（具有空标签集的记录，其中f= L）进行建模。的元素上的近似排序定义如下。底部元素近似域的所有元素。具有不相等标记的非底部元素r和RJ另一方面，具有相同标记的元素r和rJ按其嵌入函数（必须是同一域的元素）排序。象征性地，对于R中的两个非底部记录函数r，rJ，其定义在相同的Lf上，其中|如果r =（tag（{ l 1，···，lk}），{（l L，l D），（l 1，d 1），···，（lk，d k）}），则r = {l L，l 1，···，lk}|={⊥ L, l1,···,l k}, if r =(tag ({l1,···, l k}),{(⊥L, ⊥ D),(l1, d1),···,(l k, d k)})rJ=（tag（{l1，···，lk}），{（kL，kD），（l1，dJ1），···，（lk，dJk）}），其中d1，···，dk和dJ1，···，dJk当n是D中的元素时，则我们定义r±RrJ惠秩i≤k（di±DdJi）定理3.1给定一个标号为L的可数整环和一个任意整环D、 LD是一个 域。证明 参见[5]的Q定义了记录域构造函数之后，我们现在讨论它的数学性质。因为我们将使用构造域作为域上函数的最小不动点，其中所构造的域需要是Scott泛域的子域，所以我们需要确定具有在这些函数中使用所因此，我们需要证明它是其输入域上的连续函数即，作为一种功能，在域上，关于子域关系是单调的，并且在该关系下保持域的最小上界定理3.2 Domain constructor是一个连续的函数，和任意域D.证明 参见[5]的Q8M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3× ×××4签名在本节中，我们给出了类签名和相关构造的正式定义。类签名和其他签名构造是语法构造，用于捕获主流OO软件对象中的名义信息。在NOOP的对象中嵌入类签名闭包（下面正式定义）使它们成为名义对象，从而使NOOP对象成为主流OO语言（如Java [18]，C#[1]，C++[2]和Scala [24]）中对象的更精确模型。类签名形式化了对象接口的非正式概念（在[7]和[5]的第2章中讨论）。在名义上类型化的主流OOP中，类签名对应于类，它是其他对象（“外部世界”）应如何查看实例并与之交互为了捕获名义类型的主流OOP的名义信息，我们定义了三个语法签名构造：（1）类签名，（2）类签名环境，（3）类签名闭包。此外，字段和方法分别有（4）字段签名和（5）方法签名。4.1类签名如果N是所有类名的集合，L是所有成员的集合（即，，字段和方法）名称，我们定义一个集合S，其中包括所有类签名的方程(3)S= N× N× FS× MS其中和分别是叉积和有限序列集构造函数，FS=L N是字段签名集，MS=LNN是方法签名集。S的等式表示对应于某个类的类签名由四个分量组成：(i) 类名（也用作类签名的签名名(ii) 签名的直接超级签名的名称的有限序列，即，对应于类的直接超类的签名(iii) 对应于类场的场签名的有限序列，以及(iv) 对应于类方法的方法签名的有限序列在签名中使用签名名（N的成员）将类签名描述为名义构造，其中两个具有不同名称但在其他方面相等的签名是不同的签名。签名的第二个组成部分，一个（可能是空的）签名名称序列（即，是类签名的直接超级签名名称组成部分将类签名的直接超级签名的名称显式显式指定类签名的超级签名标识了直接位于命名类之上的类层次结构这也符合M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）39继承与类名相关的契约，这是在名义类型的主流OOP中要继承的内容场签名的方程表示场签名是一对字段名（L的成员）和类签名名。类似地，方法签名的等式表示方法签名是方法名、类签名名序列（用于方法参数）和签名的三元组name（方法结果）。不是集合S的所有成员都是类签名。 为了与我们关于描述类及其实例的接口的直觉相一致，S的成员s是一个类签名，如果它的超级签名命名组件，它的字段签名组件和它的方法签名组件（即，，s的第二、第三和第四个组成部分）分别没有重复的签名名、字段名和方法名（为了简单起见，我们的OOP模型中没有对方法重载进行建模然而，应该注意的是，字段名和方法名在不同的名称空间中，因此我们允许字段和方法具有相同的名称。类签名中的信息是从OO程序类的文本中派生出来的.鉴于对象的接口是OO类型系统中定义类型的基础，类签名是名义类型OO类型系统的形式基础[5]和[7]中的2，给出了OOP中类型和类型的更多细节4.2签名环境签名环境是一组有限的类签名，具有唯一的类名，其中每个签名名称与环境中除了要求签名名称的唯一性之外，有限的类签名集还需要满足某些一致性条件，以作为签名环境。 签名环境指定了签名名称之间的两种关系：直接超级签名关系和直接引用（邻接）关系（第一个关系是第二个关系的子集）。这两个关系可以表示为有向图。签名环境上的一致性条件约束这两个关系及其对应的图。因此，类签名的有限集合se是签名环境，当且仅当（i）对于se的每个类签名中的每个签名引用，具有正确签名名称的类签名属于se，（ii）se的超级签名关系的图是非循环图5，以及（iii）se中的每个类签名的字段签名和方法签名的集合是由s的超级签名分量命名的每个超级签名的字段签名和方法签名的集合的超集。与主流OO语言中的继承一致，最后一个条件使签名环境中的类签名反映显式继承4因此，函数应用符号可以用于引用签名环境中的特定类签名。如果nm是一个签名名，保证是签名环境se中某个类签名的名称，我们使用函数应用表示法se（nm）来引用这个特定的类签名。5这个约束强制任何签名环境至少有一个没有超级签名的类签名（即，它的第二个组成部分是空序列）。10M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3在基于类的OOP中，通过要求类签名只扩展（即，，添加到）由显式指定的超级签名支持的成员集要求类签名的成员是其所有超级签名的成员的超集意味着需要成员签名的精确匹配。因此，这个要求为字段和方法签名执行了一个不变的子类型规则，模仿了在添加泛型之前主流OO语言（如Java和C#）中使用的规则。这个条件可以放宽，但我们不这样做，在本文中。更多细节见[5]。4.3签名关闭在类签名中，类名可以被看作是如果没有将类名绑定到相应的类签名，则具有对其他类签名的名称引用的单个类签名本身就不是封闭实体。这激发了签名闭包的概念。类签名的闭包是一组类签名（签名环境，特别是），它将绑定绑定到集合的所有元素中引用的类名，使得整个集合在其对其他类签名的引用中没有“悬挂指针”（即，是引用封闭的），并且相对于集合中的某个主类签名（称为闭包的根类签名）没有冗余的类签名。因此，签名闭包这就促成了下面对签名闭包的正式定义签名闭包是一对签名名称和签名环境。 签名名称nm和签名环境se的对sc=（nm，se）是签名闭包，当且仅当在se中存在具有签名名称nm的类签名s，并且如果对应于se的直接引用（邻接）关系相对于s是引用闭合的，并且如果该关系是最小的这种关系。类签名s则称为sc的根类签名。相对于根类签名，签名环境是最小的，即，不包含不必要的类签名。 这个最小性条件确保了 签名闭包的签名环境可经由签名环境的邻接图中从根签名名称（对应于根签名名称的图中的节点）开始的路径访问，即，签名环境不具有对于根类签名不必要的冗余类签名类似于单个类签名，当被视为“封闭类签名”时，签名闭包有一个名称：即其根类签名的名称;有成员签名：即其根类签名的字段和方法签名;有字段形状和方法形状：即其根类签名的形状;并且它有直接超级签名名称：即其根类签名的名称。 签名闭包，而不仅仅是类签名，是对象接口概念的完整形式化表达（字段形状是字段名称的集合，方法也是如此”[7]见《易经》。[5]中的2，以获得有关形状的更多细节和对象接口的讨论基于类的OOP程序中的每个类都有一个对应的类签名和一个对应的类签名闭包。中的标称信息M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）311≡∧⇔∧⇔∧⇔ ∧ ≡ ∧ ≡ ∧≡类签名闭包是类的所有实例（包括与类名相关联的契约）的不变式。4.4关于签名的对于类签名s1=（nm1，nms1，fss1，mss1）和s2=（nm2，nms2，fss2，mss2），我们定义s1= s2（nm1= nm2）（nms1nms2）（fss1fss2）（mss1mss2）其中是序列上的等价关系，忽略了序列元素的顺序（和重复）。 对于两个场特征fs1=（a1，nm1）和fs2=（a2，nm2），fs1= fs2（a1= a2） （nm1= nm2）。类似地，对于两个方法签名ms1=（b1，nms1，nm1）和ms2=（b2，nms2，nm2），ms1= ms2 （b1= b2）（nms1=nms2）（nm1= nm2）（这里，使用序列相等，而不是序列等价。对于方法参数签名名称，顺序和重复很重要。）两个签名环境相等当且仅当它们作为集合相等。两个签名闭包相等当且仅当它们成对相等。相等签名闭包具有相同的根类签名名称和相等签名环境。最后，讨论继承时需要的签名环境之间的关系是签名环境上的扩展关系。签名环境se2扩展了签名环境se1（写为se2（se1）），如果se2将se1中定义的名称绑定到与se1完全相同的类签名。作为集合来看，se2是se1的超集。因此，在本发明中，se 2（se 1惠se 2）se 1。4.5子签名和继承类签名的supersignatures组件定义了签名闭包之间的排序关系我们将签名闭包之间的这种关系称为子签名。在基于类的面向对象程序设计中，类签名闭包之间的子签名关系是对类之间继承关系的建模如果签名环境（即，SC 2的第二组件）是SC 1的签名环境的扩展（（）），并且SC 1的签名名称是SC 2的根类签名的超级签名名称组件的成员，即，、sc2≠1sc1惠se2（se1≠（nm1∈ super_sigs（se2（nm2）.签名闭包之间的子签名关系是直接子签名关系（1）的自反传递闭包为了说明本节给出的定义，附录A给出了一些签名构造的例子，并给出了一个子签名关系中的签名闭包的例子在决定子签名关系时包含类契约使得子签名关系比结构类型化OOP中使用的结构子类型化关系更准确地反映了真正的这使得子签名捕获了这样一个事实，即名义类型OOP中的子类型化在语义上比结构子类型化更准确（如讨论中所解释的12M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3OOOOOL S LSOO×L O → O→在[7]和[5]的第2章中，Liskov替换原则和语义子类型与句法子类型）。5NOOP：一种名义型OOP使用第3节中介绍的记录域构造器（）和第4节中介绍的签名构造器，在本节中，我们现在将NOOP的构造作为名义类型的主流OOP的更精确模型NOOP的建设分两步进行。首先，一个简单的递归域方程的解定义了原始对象的初步域闭包，其中一个域闭包中的对象包含（1）编码标称信息的签名闭包 名义类型的OOP，并在两个单独的记录中包含对象成员的绑定对具有签名信息的对象的简单递归定义并不强制嵌入在对象中的签名信息与其成员绑定一致因此，在构造NOOP的第二步中，所构造的初始的objuO域被领域的适当对象模型的名义对象的主流面向对象软件。无效对象是签名信息与成员记录中的成员绑定不一致的对象初始域的过滤是通过定义初始域上的投影函数。我们称具有由域方程我们的目标模型NOOP是一个包含图像域的模型，该图像域是通过在初始域上应用滤波函数得到的。在NOOP之前。5.1建设NOOP定义preNOOP和NOOP的域方程使用了两个可伸缩域和。 Domain是标签的可扩展域，Domain 是一个 签名闭包域（第4节）。描述前NOOP的域方程为：（4）O=S ×（LO）×（L（O→O））其中，由等式定义的主域是原始对象的域是严格产品域构造函数，是记录域构造函数（第3节）。等式（4）指出，每个原始对象（即，，每个元素都是一个三元组：(i) 签名封（即，S的成员），(ii) 一个字段记录（即，，a me mberofLO），以及(iii) 方法记录（即，，我很高兴，（其中，是严格连续函数域构造函数，并且是有限序列域构造函数）。M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）313OOOO OOOOOO›→···p reNOOP的DomainO是方程（4）的解。应用迭代根据域理论[12]的最小不动点（LFP）构造方法，在方程（4）的方程的RHS被看作是一个连续函数，定义域上的连续性（给定所有使用的域构造函数的连续性，并且构造函数组合保持连续性。前NOOP的迭代构造的细节在[5]中给出构造NOOP的第二步是定义一个投影/过滤函数，filter，将preNOOP的域映射到有效对象的NOOP域，有效对象对名义类型的OOP对象进行建模。 为此，首先，我们在O中定义一个对象，使其有效如下。定义5.1如果对象o是底部对象，或者如果它是非底部对象o=（sc，fr，mr），• sc的场形状和方法形状分别与fr的形状和mr的形状• 绑定到fr中的字段名的非底部有效对象具有签名闭包，该签名闭包子签名sc中对应字段的签名闭包，并且• 绑定到mr中方法名的非底层函数符合sc中相应的方法签名。通过一致性，函数需要接受有效对象的序列，其嵌入的签名闭包子签名（组件方式）sc中的方法参数签名闭包的相应序列，并以sc本身作为前缀（对于隐式参数self/this），并返回具有签名闭包的有效对象，该签名闭包子签名sc中的方法签名中指定的相应返回值签名闭包。将Oin映射到O（O是O的一个恰当子域）的函数滤子是使用以下三个递归函数定义来定义，使用lazy函数式语言伪代码。有趣的过滤器（o：）：将o与（（nm，se），fr，mr）如果（sf-shp（se（nm））！= rec-shp（fr））（sm-shp（se（nm））！= rec-shp（mr））return//不匹配的形状else//lazy构造最接近o匹配se（nm）、fr、mr，（_，_，[（ai，sn mi）|i =1，· ··，m]，[（bj，m i_snmj，mo_sn mj）|j=1，· ··n]），（fr-tag，{ai oi|i =1，· ··，m}），（mr-tag，{bjm j|j =1， ，n}）设si = se_i（se，snmi）设misj = map（se_snm（se），[nm：：mi_snmj]）//nm被前置到mi_snmj以处理设mosj = se_snm（se，mo_snmj）∨14M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3SS OOS S MMOOOO OOOOreturn（（nm，se），（fr-tag，{ai› →filter-obj-sig（si，oi））|i=1，· ··，m}），（mr_tag，{b_j}→filter_meth_sig（misj，mosj，m_j）| j=1,· ··,n}))funfilter-obj-sig（ss：，o：zh）：将o与（s，_，_）匹配if（s）returnfilter（o）//最接近o的有效对象其他returnbrowser//没有子签名funfilter-meth-sig（in_s：+，out_s：，m：z h ）：return（λos. 设vos = map2（filter-obj-sig，in_s，os）在filter-obj-sig（out_s，m（vos）在过滤器的定义，函数sf-shp和sm-shp计算签名的场和方法形状，而函数rec-shp计算记录的形状。函数se_numb（se，nm）计算对应于签名名称nm的签名闭包，其第一个分量是nm，其第二个分量是使se_numb（se，nm）成为签名闭包的签名环境se的最小子集。要处理this/self，将se_self的“curry”版本传递给map函数。另外，domain+是签名闭包的非空序列的域（非空是因为方法总是至少在对象this/self中传递），域M和M是方法和方法的辅助域，- 是的函数map2是map的二维版本（即，，接受一个二元函数和两个输入列表作为其参数）。换句话说，filtering函数filter的定义是，该函数接受一个对象o，并返回一个对应的有效对象。如果对象由于o及其成员记录的签名闭包中的形状不匹配而无效，则filter返回bottom对象(in域 你好，是与在其签名和记录中具有不相等形状的无效对象最接近的有效对象）。否则，o有匹配的签名和记录形状，但可能有对象绑定到它的字段，或者被它的方法接受或返回，其签名闭包不对o的签名闭包中对应的签名闭包进行子签名。在这种情况下，filter会延迟构造并返回域中最接近的有效对象。到o，其中o的所有非底部字段和非底部方法都被保证（分别通过函数filter-obj-sig和filter-meth-sig）具有签名闭包，该签名闭包子签名o的签名闭包中的相应签名闭包。函数filter-obj-sig检查其输入对象o是否有签名闭包s，该签名闭包s子签名所需的声明签名闭包ss。 如果s不是ss的子签名，则返回filter-obj-sig。如果是，则函数在o上调用filter，从而返回最接近o的有效对象。对于方法，当filter-meth-sig应用于方法m时，它返回一个有效的M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）315O∈OO⊥O方法，当应用于与m相同的输入os+时，返回m的输出对象的最接近的有效对象，该对象将声明的输出签名闭包out_s添加到与最接近（组件方式）的有效对象序列相对应的有效对象中，该有效对象（再次，组件方式）将声明的输入签名闭包in_s的序列添加到前缀有封闭m的对象的签名闭包中（以正确地填充os中的第一个参数对象，这是this/self的值）。在[ 5 ]中证明了定义为过滤器的域是O的定义良好的可计算子域。5.2类类型正如所构造的那样，NOOP是OOP的一个名义模型，因为域的对象包括指定由对象维护的相关类契约（包括继承的契约）的签名。这种编码在签名中的名义信息提供了一个框架，用于自然地将NOOP对象的域划分为定义类类型的集合，其中类型是一组相似对象。首先，我们定义精确的类类型。对应于类C的确切类类型是用C的签名闭包标记的所有对象的集合 6接下来，应该注意的是，名义类型的主流OOP的一个基本原则是，来自类C的子类的对象符合类C的契约，并且可以用来代替使用类C构造的对象（即，，代替C的确切类类型中的对象）。因此，与类C相关联的自然类型，称为对应于C或由C指定的类类型，由类C中的对象加上类C的所有子类中的对象 在名义类型的OO语言中，类C指定的类类型不是C的确切类类型，而是与子类（即子类）相对应的所有确切类型的联合。，继承自）类C，包括类C本身。受此讨论的启发，我们将NOOP中的类类型定义为签名闭包的解释。对于签名闭包sc，它的解释S[sc]是域O的子域，具有域O的相同的底层近似序，并且其论域由以下等式定义：(5)|={（scs，fr，mr）∈ O |scs sc }{O }。|scs Ð sc}∪ {⊥ O}.换句话说，由类指定的类类型是对应于类的签名闭包sc的解释，而签名闭包sc又是NOOP域中具有签名闭包scs的所有对象的集合，该签名闭包scs子签名sc或底部对象O。考虑到NOOP中的子签名模型是面向对象的继承，NOOP类类型的定义完全符合主流面向对象开发人员的直觉。5.3继承 是子类型在构造了NOOP并基于主流OO开发人员的直觉定义了类类型之后，我们现在可以很容易地看到它对名义类型的6例如，在Java中，类C的确切类型的对象正是getClass（）方法返回C的类对象16M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3⊆∈OO我的天{→O···<$→O}{<$→M···→M}{···}主流OO类型系统完全识别继承和子类型。我们将此声明形式化地表示如下：对应于两个类的两个签名闭包通过两个签名闭包处于子集关系（即，，这两个类是当且仅当对应的类类型在名义子类型化关系中时）。我们在下面的定理中证明了继承和子类型之间的对应关系定理5.2对于表示类类型S[sc1]的两个签名闭包sc1和sc2而S[sc2]，我们有(6)sc1惠sc2惠S[sc1]惠S[sc2]证明基于等式（5）和类类型7的非空性，该定理的证明很简单。Case：方向：如果sc1≠sc2，则通过应用S[sc2]的定义（等式（5）），S[sc1]属于S[sc2]（等式（5）中的变量scs被实例化为sc1，并且在所有的类类型中，都是一个通用的成员）。 因此，S[sc1]=S[sc2]。Case：如果（If）方向：通过S[sc1]的非空性，存在具有签名闭包sc1的S[sc1]的非底部对象o。如果S[sc1]S[sc2]，则OS[sc2]。通过等式（5），S[sc2]的所有非底部成员必须具有子签名sc2的签名闭包。当应用于o时，我们因此得到sc1<$sc2。Q在上面的证明中我们应该注意到，这是NOOP对象的名性（即，将签名闭包嵌入到对象中），这使得S[sc2]是S[sc1]的超集，这意味着sc1将sc2作为其超级签名之一，反之亦然。证明的简单性清楚地表明了类签名和类类型定义的自然性。6结论在本文中，我们提出NOOP作为一个模型的面向对象程序设计，其中包括名义上类型的主流面向对象软件中发现的名义信息。这使我们很容易地证明，继承，在语法层面上，和子类型，在语义层面上，完全同意名义类型的OOP。因此，我们相信，在任何名义类型的主流OOP的精确模型中，都有通过包含名义信息，NOOP提供了一个机会来理解和推进OOP和基于更坚实的语义基础的当前OO语言。7类类型S [sc]总是非空的（即，总是具有某个非底部对象），因为对象（SC，A1，A M ，B1，，bn）（其中a1，，m是场的形状，sc和b1，bn是sc的方法形状）总是有效的构造对象（即，，是preNOOP的域过滤的对象，它将过滤传递到NOOP的域）。该对象是等式（5）的S[scM.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3177今后工作研究的可能性，可以建立在研究的顶部，这张纸有很多。一个近期可能的工作是定义一个最小的名义类型的OO语言，例如。在FJ[20]的基础上，以标准的直接方式给出了该语言在NOOP中程序结构的指称语义。这种语言的类型安全性可以使用给定的指称语义来证明。另一个可能的未来工作，可以建立在NOOP的顶部是产生一个指称模型的泛型名义类型的OOP。这样的模型可以为更好地分析名义类型的主流OO语言中的泛型特征提供机会，从而为建议改进和扩展这些语言的类型系统确认作者非常感谢Robert“Corky”Cartwright教授作者还想把这部作品献给他已故的亲爱的母亲。她一直是一个非常激励的灵魂，是他的主要支持者在本文提出的研究发展。妈妈，我很想你。引用[1] C#语言规范，版本3.0。 http：//msdn.microsoft.com/vcsharp，2007年。[2] ISO/IEC 14882：2011：编程语言：C++。2011年。[3] 马丁·阿巴迪和卢卡·卡德利 对象类型的语义。 在Proc.LICS[4] 马丁·阿巴迪和卢卡·卡德利 对象的理论。Springer-Verlag，1996.[5] 莫兹河AbdelGawad NOOP：面向对象编程的数学模型。博士论文，莱斯大学，2012年。[6] 莫兹河AbdelGawad 在名义类型的面向对象编程中，对象不仅仅是记录，继承是子类型。2013年提交出版。[7] 莫兹河AbdelGawad面向对象编程中的名义类型与结构类型的概述。技术报告，arXiv.org：1309.2348[cs.PL]，2013年。[8] 金湾布鲁斯面向对象语言的基础：类型和语义。麻省理工学院出版社，2002年。[9] 卢卡·卡德利多重继承的语义。在国际上，Symp.关于数据类型的语义，第173卷，第51-67页。Springer-Verlag，1984.[10] 卢卡·卡德利 多重继承的语义。 告知。 的Comput。，76：138[11] Robert Cartwright和Moez A.AbdelGawad 继承是子类型（扩展抽象）。在第25届北欧编程理论研讨会（NWPT），塔林，爱沙尼亚，2013年.[12] 罗伯特·卡特赖特和丽贝卡·帕森斯Domain Theory：An Introduction，1988. 专著（基于Dana Scott的早期注释18M.A. AbdelGawad/Electronic Notes in Theoretical Computer Science 301（2014）3[13] William R.厨师. 继承的指称语义。 布朗大学博士论文，一九八九年[14] William R.作者：Walter L. Hill，and Peter S.坎宁继承不是子类型。在PO