面向对象的和弦语言SCHOOL：操作语义和类型系统的形式化模型

理论计算机科学电子笔记135（2006）37-47www.elsevier.com/locate/entcsSCHOOL：一种小型的Chorded面向对象语言S. Drossopoulou，A. Petrounias，A. Buckley，S. 艾森巴克{s.drossopoulou，a.petrounias，a.buckley，s.eisenbach}@imperial.ac.uk英国伦敦帝国学院计算系摘要Chords是一种基于Join-calculus的声明式同步构造，可在编程语言C-omega中使用。据我们所知，和弦在面向对象的环境中没有形式化的模型。在本文中，我们提出了一个形式化的模型SCHOOL，一个命令式的，面向对象的和弦语言。我们给出了一个操作语义和类型系统，并证明了该类型系统的可靠性。保留字：和弦，连接，并发，面向对象，语义1引言一个和弦程序[1]由类定义组成，每个类定义一个或多个和弦。一个和弦有一个签名和一个身体。chord当对象已经接收到针对chord的同步和异步方法签名中的每一个的至少一个消息时，执行chord主体。可能需要多个方法调用来调用chord的主体。这反映了Join演算[3]中join的概念，其中join模式由包含chord签名的方法组成例如，下面的和弦，一个无界的buffer：public int findDuplicate（int x;}1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.01938S. Drossopoulou等人/理论计算机科学电子笔记135（2006）37将执行主体并返回x，只有当同时存在对其签名中的两个方法的调用get方法是同步的，因此会阻塞它的调用者，直到有一个消息出现在put方法上，因此它可以加入。后一个方法是异步的，是void的一个子类型，并立即返回到它的调用者;因此发送给它的消息必须由接收对象排队，直到被chord的连接消耗。那些签名包含同步方法的和弦称为同步和弦。只有异步方法的Chords被称为异步chords。2语义学我们以结构化操作语义（见图2）和伴随的类型系统（见图3）的形式呈现SCHOOL（见图1中的概述）这篇论文的扩展版本，包括额外的材料，更全面的和弦覆盖，以及手写的可靠性证明，可以从以下网站找到：slurp.doc.ac.uk/school。表达式和程序SCHOOL 表 达 式 的 语 法 是 ： 方 法 调 用 ， 表 达 式 序 列 ， 接 收 器（this），参数（x），以及值null（用于空指针）和voidV al（用于返回void的执行结果或用于调用异步方法的结果）。我们还定义了SCHOOL程序，它是映射的元组。我们没有给出程序的语法，因此可以省略那些查找方法和超类的派生函数的机械定义。一个程序包括：1）从类和方法名到该类中方法4）从类名到它的超类名的映射一个方法签名包含一个返回类型、一个方法名和一个参数类型.形参的名字是从方法的名字派生出来的：对于一个名为mth的方法，形参将被称为mth x。当然，这些限制对于编程来说是不方便的，但不是必需的我们的和弦和类型的研究，他们允许一个相当简洁的介绍。我们将chord表示为一组异步方法名称以及表示chord主体的表达式。A之间的区别S. Drossopoulou等人/理论计算机科学电子笔记135（2006）3739同步和弦和异步和弦的区别在于和弦是出现在SCHOOL节目的第二还是第三组件的图像中。方法名称可以出现在任意数量的和弦中。为了便于记法，我们还定义了以下四个查找函数：函数M（P，c，m）是P的第一个分量的投影，并返回m函数AChs（P，c）是P的第三个分量的投影，并返回类c的异步和弦的集合;最后，Ma（P，c）给出了类c的和弦定义中存在的所有异步对象、消息和堆可以将chord调用视为对象之间的消息传递。调用者对象向接收者对象发送包含名称和参数的消息。对异步方法的调用会立即返回，但相应的chord主体可能尚未准备好运行。因此，以异步方法为目标的消息在接收器对象中排队。因此，一个对象包括1）它的定义类的名称，2)一个队列用于其类中的每个异步方法签名。因此，对象的状态由其队列表示异步方法被建模为从方法标识符到多组值的映射，这些值表示调用异步方法时传递的实际参数。多集的使用允许处理异步方法调用的非确定性本质的自然呈现，由此异步调用不能保证按照它们进行的顺序进行处理，即使它们是从同一线程连续进行的[1]。我们需要multisets而不是sets来模拟异步方法被同一个参数调用两次一个有趣的现象是，任何可以访问另一个对象的对象都可以通过调用异步方法写入其队列。但是，只有与异步方法签名关联的chord主体才能从方法的队列中读取。从队列中读取会消耗其中一个元素。堆将地址（以N为单位）映射到对象。一旦一个对象被分配到一个地址上，就没有办法移除它了。因此，就地址到值的映射而言，堆单调增长。但是，每个对象中的队列会随着消息发送到队列和从队列中使用而增长和收缩， 如前所述。操作语义40S. Drossopoulou等人/理论计算机科学电子笔记135（2006）37图2中的SCHOOL操作语义与[2]的风格相同这些规则的目的是尽可能地从日程安排中抽象出来，越好.因此，只要有选择，我们就欢迎非决定论，从而最大限度地提高程序的可能行为。 有三条规则特别感兴趣的是：ASYNC，JOIN和STRUNG。 这三条规则学校里的和弦调用的本质同步描述了异步方法的调用：表示void的值立即返回，实际参数被放置在接收对象的相应队列中。JOIN描述了同步方法的调用调用方将阻塞，直到包含传入的方法的chord中存在的所有异步方法在其各自的队列中至少有一条消息，接收对象。注意chord的选择是不确定的，参与队列元素的选择也是不确定的。一旦chord连接，消息就从队列中消耗，当前表达式成为chord的主体。STRUNG描述了异步和弦的执行由于没有调用者等待和弦加入，因此（抽象）调度器负责决定选择哪个和弦。从本质上讲，这个规则在三个层次上展示了非确定性选择：堆中对象的选择，异步和弦的选择以及从分离队列中的元素的选择chord的主体将在新线程中执行（我们称之为spawning）。类型判断判断P， h_e：t描述源级表达式e的静态类型，而判断P，h_e：t描述运行时表达式e的动态类型。完整的SCHOOL类型系统可以在图3.格式良好的程序一个格式良好的SCHOOL源程序（WF-PRGM）由格式良好的类声明（WF-C类）组成如果一个类的超类是一个类，那么这个类声明就是格式良好的，即，对象或在程序中定义的类，从超类重写的任何方法都具有相同的签名，直到dec或void，所有同步和弦都是格式良好的，所有异步和弦都是格式良好的。当和弦的同步方法签名的返回类型与和弦主体的类型一致时，同步chord body是在一个上下文中类型化的，其中形式参数采用类型men-S. Drossopoulou等人/理论计算机科学电子笔记135（2006）3741在同步和异步方法签名中，这将采用当前类的类型。chord签名中的任何其他方法签名都当和弦主体具有类型void时，异步和弦是格式良好的，当在形式参数采用异步方法签名中提到的类型的上下文中键入时。关于方法覆盖，我们的系统允许一个返回void的方法在子类中被一个返回void c的方法覆盖。 它还允许一个返回void的方法在子类中被一个返回void的方法覆盖。 Cω只允许返回void被一个返回blog的方法覆盖。虽然我们允许的重写可能不是好的编程实践，但它并不影响类型系统，因此是允许的。此外，Cω对涉及chord的方法的重写施加了限制，以避免继承异常[4]。然而，固有异常与同步特性的保持有关，与类型可靠性无关。因此，我们的制度并没有作出类似的限制。最后，我们不要求类层次结构是非循环的。虽然此属性对编译器很有用，但它对类型的可靠性不是必需格式良好的堆格式良好的堆（WF-Heap）要求对象队列中的每个值都健全性SCHOOL的求值规则在整个执行过程中保留类型。我们通过一个主语归约定理证明了这个性质[5]。证明技术是标准的。我们首先定义适当的替换σ，它以类型保持的方式将标识符映射到地址上。定义2.1[适当替代]对于置换σ=Id<${this}−→Addr、堆h和堆Γ，我们有：dom（r）=dom（σ）Γ（id）=c=π，hσ（id）：c=r，hσ我们可以很容易地证明，当对表达式e应用适当的替换σ时，它会将其转换为与42S. Drossopoulou等人/理论计算机科学电子笔记135（2006）37⎪原创表情引理2.2（替换）ΣP，Γe：tP，h ►σ=P，h[e]σ：t证据 通过对表达式e的归纳。Q此外，如果一个运行时表达式在堆h中具有某种类型，那么它在任何堆hJ中都保留其类型，其中对象与h中对应的对象具有相同的类。引理2.3（保存）如果：dom（h）：h（i）=[c||]]=h′（i）=[c||--则：P，h′e：t=P，h ′e：t证据通过对表达式e的结构归纳，Q我们可以证明顺序情况下的主语归约：Lemm a 2. 4（无约束力的教育研究-S方程）P 拉克什► P⎪⎪普什赫=P，he：t⎪e，h~e′，h′P，h′e′：t证据 通过结构归纳法推导出~。Q最后，我们可以证明多线程情况下的主题归约定理2.5（主题归约-线程）对于SCHOOLheapshandh′，prgramP，express ionse1，. . en，e′，.. .e′，类型T1，.tn，1m如果：• 普和普，• e1，.. . ，en，h~e′，. ，e′，h′1m• P，h ei：ti n则存在类型t′，. ，t′以便：• 帕赫• P，h′e′：t′1mi ∈ 1.. M我我• {t1， ...， tn}{void}={t′， ...，t′{void}1m证据 通过对~的案例分析和引理2.4的应用。Q⎪S. Drossopoulou等人/理论计算机科学电子笔记135（2006）37433结论和未来工作我们设计SCHOOL的目的是研究在命令式、面向对象的环境中理解和弦所必需的功能。我们做出了各种设计决策，以保持我们的语言简单和描述最小化。因此，只有类和和弦是必要的;操作语义只需要半页，十条规则！我们还在SCHOOL中引入了子类，因此能够正式确认，尽管继承和同步通常不能很好地混合[4]，但这些问题与类型可靠性无关。 因此在我们允许一个返回void的方法被一个返回void的方法覆盖，反之亦然。我们还允许在一个chord中定义的方法成为子类中另一个chord的一部分。Cω中对重写和方法声明的限制因此与打字问题无关;相反，试图保留方法在子类中的同步方式。在进一步的工作中，我们希望扩展SCHOOL来研究与其他语言功能的有趣交互。尽管泛型、包、内部类、重载和各种控制结构等特性可能与chord正交，但我们预计委托和异常的引入可能会引发一些有趣的问题。更有趣的将是SCHOOL和Java和C中的显式同步机制（如锁和监视器）的组合研究。此外，我们想设计扩展的和弦，以纳入更先进的功能，如抢占，优先级和交易。我们将用学校来表达我们的设计。这也将是有趣的考虑问题周围的调度和弦。SCHOOL的语义是非确定性的，因此抽象出和弦的一个重要属性，如复调C;即任何可以运行的和弦（即， 其队列不是空的），最终将运行。人们可以尝试通过进一步细化操作语义来验证这种公平执行策略。更有趣的是对特定调度机制的正式理解，以及它们的属性的证明。最后，另一个具有挑战性的方向是在程序理解和验证中使用和弦在[1]中，异步方法对应于状态，一些同步方法调用对应于状态变化。虽然这种类比不能期望总是成立，但研究如何将状态转换图映射到Chorded程序，反之亦然，这将是有趣和有用的。这样的方法将允许应用模型检查器。44S. Drossopoulou等人/理论计算机科学电子笔记135（2006）37引用[1] 本顿，N.，L. Cardelli和C. Fournet，面向C语言的现代并发抽象，ACM Trans.Program。26（2004），pp. 769-804.[2] Drossopoulou ， S. ， Java 动 态 链 接 和 加 载 的 抽 象 模 型 ， 在 ： R 。 Harper ， editor ， ThirdInternational Workshop，Types in Compilation（TIC 2000），LNCS2071（2000）.53比84[3] 富尔内角和G.Gonthier，The reasonexive CHAM and the join-calculus，in：Proceedings ofthe 23rd ACM Symposium on Principles of Programming Languages（1996），pp.372-385.[4] 松冈S.和A. Yonezawa，面向对象并发编程语言中继承异常的分析，在：面向对象并发编程的研究方向（1993），pp. 107-150[5] Wright，A.K. 和M.Felleisen，A syntax approach to type soundness，Inf.Comput. 115（1994），pp. 38比94S. Drossopoulou等人/理论计算机科学电子笔记135（2006）3745抽象函数es ∈ ExprS：：=null|voidVal|这|X|新的c|es.m（es）|es;esMethSig：：=t m（c）t ∈类型：：=虚空|async| cx，c，m ∈ IdM（P，c，m）=P↓1（c，m）SChs（P，c，m）=P↓2（c，m）AChs（P，c）=P↓3（c）是个：程序× Idc→ P（Idm）是个 ={m| M（P，c，m）=<$c m（）}程序表示实体程序=Idc×Idm→MethSig×Idc×Idm → P（Chord）×Idc→ P（Chord）×IDC →IdcChord=P（Idm）×Expr格式良好Pcocl =Pc► PPP↓4（c）oclWF-PRGMM（P，P↓4（c），m）=t m（tJ）=<$M（P，c，m）=tJJm（tJ）其中tJJ=t或t，tJJ∈{void，<$c}SChs（P，c，m）$（{m 1，.，mn}，e）=i ∈ 1.. n：n ti：M（P，c，mi）=n cmi（ti）t，tJ：M（P，c，m）=t m（tJ）P，（m1 x→ t1，. ..， mnx<$→tn，m x<$<$→tJ，this<$→c）e：tAChs（P，c）$（{m 1，. ..，mn}，e）=i ∈ 1.. n：n ti：M（P，c，mi）=n cmi（ti）P，（m1 x→ t1，. ..， mnx<$→tn，this<$→c）e：voidPP PPWF-C玻璃h（i）=[c||qs]]，M（P，c，m）= cm（t），v∈qs（m）=<$P，h<$v：t帕赫WF-HEA pFig. 1.学校概况堆=N→对象对象=ID C ×阿斯图里亚斯队列=Idm→ multiset（ Val）e∈ Expr：：=voidV al|nullPtrEx |v|新的c| e.m（e）|e;ev∈ V ali∈N：null|ι46S. Drossopoulou等人/理论计算机科学电子笔记135（2006）37上下文E [. ]* = E [. ].m（e）|m（E [. ]中）|E [. ] 的一种;ee，h~eJ，hJE [e]，h~E[eJ]，hJ评估规则r∈N<${null，voidV al}CNTX休息;e，h~e，hSEQ{e 1，. . .，en}={eJ，. . .，eJ}1ne n，h~eJ，hJnPRUNe1，. . .，en，h~eJ，. . .，eJ，h1ne1，. ..，en，h~e 1，. . .，en−1，eJ，hJnEXEX-PROpnull. m（v），h~ nullPtrEx，hE [nullPtrEx]，h~nullPtrEx，hh（i）=UdfMa（P，C）={m 1，. . .，mn}NEW新C，h~i，h[i›→[[ C||M 1 →，. . .，mn]]]h（i）=[c||qs]]M（P，c，m）= c m（）同步I. m（v），h~voidV al，h [i] → [[c||qs [ m → {v}qs（m）]h（i）=[c||qs]]SChs（P，c，m）$（{m 1，. ..，mn}，e）i ∈ 1.. n：qs（mi）={vi}<$qi加入链接I. m（v），h~e [v1/m1x，. . .，vn/mnx，v/m x，i/this]，h[i] →[[c||qs[m 1 ›→q 1，. . .，mn ›→qn]h（i）=[c||qs]]AChs（P，c）$（{m 1，. . .，mn}，e）i ∈ 1.. n：qs（mi）={vi}<$qi斯仲e1，. ..，ek，h~e 1，.，ek，e[v1/m1x，. . .，vk/mkx，1/this]，h[i] →[[c||qs[m 1 ›→q 1，. ..， Mn ›→qn]图二. SCHOOL操作语义S. Drossopoulou等人/理论计算机科学电子笔记135（2006）3747类和类型声明P↓4（c）/=UdfDEF-C类-1DEF-C级-2公司简介P对象t∈ {void，c}Pc oclDEF-TY pE-1 DEF-TY pE-2PtotpPcotp源级类型判断Pcoclz∈ {this}ST-NULLST-VOIDST-T他的XP， r=null：cP， r =voidP，Γz：Γ（z）公司简介ST-NEWP， r=new c：cP，Γε1：cP，Γε2：tM（P，c，m）=trm（t）ST-I系列P，r= 1. m（e2）：trP，r=1：t 1P，r_e2：t 2ST-SEqP，Γε1 ;e2：t 2运行时类型判断公司简介h（i）=[c||]]RT-NULLRT-VOIDRT-ADDRP，hnull：cP， hvoidP，h：c公司简介RT-NEWP，hnew c：cP，h1：cP，h2：tM（P，c，m）=trm（t）RT-I系列P，he 1. m（e2）：trP，h1：t 1P，h2：t 2RT-SEqP，he1;e2：t 2P，he：cP↓4（c）=cJP，he：cJP，he：voidRT-SUB-A同步P，he：cPtotpRT-EXRT-S ub-CLSP，h►nullPtrEx：t图三.学校类型系统