多线程Java：异常断言证明系统

理论计算机科学电子笔记159（2006）281-297www.elsevier.com/locate/entcs在多线程Java1中实现可重用性的归纳证明大纲ErikaA'bra h'am2Albert-Ludwigs-UniversityFreiburg，德国弗兰克·S de Boer4CWI阿姆斯特丹，荷兰Willem-Paul de Roever和Martin Steffen3InstitetforComputerScienceanddAplieddMathematics，Christian-Albrects-Univrsi t？t üatzuKiel，德国摘要在本文中，我们给出了一个操作语义，并介绍了一个多线程Java子语言中的异常断言证明系统。保留字：Java，多线程，异常，证明系统1介绍在这项工作中，我们提出了一个断言证明系统的多线程子语言的Java，包括对象和线程的创建，别名，方法调用，1这项工作的一部分得到了IST项目Omega（IST-2001-33522）的资助，见http：//www-omega。我是G。和NWO/DFGprojtMobi-J（RO1122/9-{1，2，4}）。2个月前：一个月前。联合国-国际自由贸易组织。De3分钟后：{wpr，m s}@infor m atik. 联合湖。De4个月前：frb@cwi. nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.072282E. Abraham等人/理论计算机科学电子笔记159（2006）281因此，Java的系统将继承和子类型化作为一个整体，并将继承和子类型化作为一个整体，但忽略了继承和子类型化的问题。证明系统是健全和相对完整的，并且还允许证明死锁自由[3]。验证过程分为三个阶段：首先，程序被新的辅助变量扩充，并以Floyd [8，9]的风格用断言进行注释，当控制流到达注释点时，断言在程序执行期间保持不变之后，证明系统，应用于增强和注释的程序，也称为证明大纲[18]，产生许多验证条件，确保每个程序执行符合注释。最后，必须证明验证条件。我们使用[19]这是一个很好的例子。通过用户提供的增强和注释，Verger工具负责第二阶段的验证条件生成。定理证明器中的实际验证是交互式的。对于我们所做的例子，大多数条件都可以使用PVS的内置证明策略自动解除。人类的互动主要是为了证明那些需要量词的性质。为了支持内部和外部对象对象间的干净接口，我们排除了对实例变量的限定引用。因此，共享变量并发性是由单个对象内的同时执行引起的，而不是跨越对象边界。 为了反映程序行为的这种模块性，断言逻辑和证明系统在两个层次上进行了仿真，一个是用于内部对象行为的局部层次，另一个是用于描述全局行为的全局层次，包括对象的通信拓扑。证明系统的验证条件保证了程序的正确性除了初始正确性之外，这些被分组如下。单个方法体的执行是通过使用本地语言的本地正确性条件来捕获同时执行的方法之间的干扰由干扰自由度测试[13，18]涵盖，也用当地语言制定。它尤其需要容纳重新进入的代码和同步机制。可能影响多个对象，通信和对象创建由合作测试覆盖，使用全局语言。通信可以发生在单个对象内或不同对象之间。由于这些情况无法在语法上区分，因此我们的合作测试结合了[5]和[13]中用于CSP的类似规则的元素这一工作通过异常处理扩展了早期的结果[2]据我们所知，这是第一个健全的和相对完整的断言证明方法的并发Java子语言，包括同步和异常E. Abraham等人/理论计算机科学电子笔记159（2006）281283装卸.面向对象程序验证领域的研究主要集中在顺序语言上。特别是，有几个工程处理例外和相应的证明理论。然而，虽然并发和异常的概念可以独立理解，但两者的结合需要仔细检查相互作用：证明系统必须在异常处理期间额外容纳交叉方面特别是，我们需要细化的规范（增强和注释），允许在异常处理过程中描述所有交织点此外，除了异常控制结构的局部正确性之外，我们还需要扩展验证条件以涵盖异常处理期间的干扰以及由于异常返回而引起的通信虽然本文的介绍集中在例外情况，规则也代表了整个证明系统有关并发。例如，LOOP项目[10，14]开发了使用PVS和Is- abelle/HOL验证顺序面向对象语言的方法和工具。特别是[12，11]形式化了Java的异常机制。Poetzsch-HeffteranddMuller[21]为Java的顺序内核提供了一个Hoare-stylepram minglogi c。翻译的操作和公理语义到HOL定理证明允许计算机辅助的合理性证明。在[22]中，JavaCard的一个很大的子集，包括异常处理，在Isabelle/HOL中被形式化，并且在定理证明器中显示了它的可靠性和完整性在[16]中，给出了定理证明器ACL 2中JVM简化版本的可执行形式化。关于例外机制的早期正式说明，[6]或[15]。本文的其余部分组织如下：在第2节和第3节介绍了程序设计语言和断言语言之后，主要的第4节定义了证明系统。第5节包含一些结论性的重新标记。2编程语言2.1语法虽然我们在这项工作的理论部分使用抽象语法（参见图1），但我们的工具支持Java语法。该语言是强类型的;除了类类型c，我们还使用布尔和整数作为基本类型，并使用pairs和list作为复合类型。如果不引起混淆，我们就省略类型。程序是包含方法声明的类的集合。我们在语法上区分类的实例变量x和方法的局部变量u;y表示任意变量。我们省略了语法变量284E. Abraham等人/理论计算机科学电子笔记159（2006）281e：：= x|u|这|null|f（e，. . .，e）eret：：=|estm：：= x：= e|u：= e|u：= newc|u：= e.m（e，. . .，e）、|e.m（e，. . .， e）、|尝试stm catch（c u）stm。|try stm catch (c u) stm. . . catch（cu）stm finally stm yrt|短链霉菌|ife then stm else stm fi|而E做STMOD。|while e do stmod. . .改性 ：：= nsync|同步meth：：= m（u，. . 、.、u）{stm; return eret}methrun：：=nsync run（）{stm;return}methpredef：：=methstartmethwaitmethnotifymethnotify Allclass：：= class c{meth. . . meth methrunmethpredef}classmain：：=classprog：：= class. . . class classmainclassFig. 1. 程序设计语言的抽象语法声明，并假设每个变量都是适当类型的。一个类的实例变量集是由该类中出现的实例变量隐式给出的，方法的局部变量也是如此注意，我们不允许在表达式e中使用限定引用e.x。语法包括用于通常的控制结构的语句，特别是用于抛出和处理异常的语句。我们使用bodym，c来表示类c的方法m的body，它必须由一个return语句终止。方法可以分别使用调制器nsync和sync声明为非同步或同步5每个类都包含预定义的start方法，预定义的monitor方法wait、notify和notifyAll，以及一个用户定义的方法run。对于预定义方法的语法定义，请参见[2]。主类的run方法指定程序的入口点。我们要求块catch（c u）stm中的局部变量u不会出现在catch块之外的同一个方法中。此外，对象创建和方法调用语句可能不包含实例变量，5Java没有non-synchronized修饰符;默认情况下，方法被声明为non-synchronized。E. Abraham等人/理论计算机科学电子笔记159（2006）281285inst参数不能被分配。6不能直接调用run2.2语义2.2.1状态和配置在语义中，我们添加类型Object作为所有类的超类型注意，不能创建Object类型的对象，因此保持单态。设Valt是各种类型t的不相交域。 对于类名c，我们使用α，β，. . . Val ∈c作为对象标识符的典型元素。nullintypec的值是null c∈/Val c。类c的方法m的局部状态τm，c（或简称τ）保持该方法的局部变量的值。 这是一个不完整的地方，它不是由它决定的。对象α / = null的方法的局部配置（α，τ，stm）指定其局部状态τ和由语句stm表示的控制点。一个线程配置是一个栈（α0，τ0，stm0）。. . （αn，τn，stmn），其表示a hr e a d的调用chain。为了将一个新的局部填充图输出到堆栈上，我们编写了一个函数（α，τ，stm）。一个对象的特征是它的实例状态σinst，它给自引用和实例变量赋值初始实例状态由σinit表示。全局状态σ为每个当前存在的对象α存储其实例状态σ（α），具有不变性质σ（α）（this）=α。一个全局配置T，σn通过全局状态σ描述当前存在的对象，其中集合T包含所有当前执行线程的配置表达式在实例状态和局部状态的上下文中计算其中，m为[[x]]σinst，τ=σ（x）和[[u]]σinst，τ=τ（u）。EinstE局部状态τ[u<$→v]通过将值v分配给变量u;σinst[x<$→v]是相似的，σ[α.x<$→v]通过将v赋给对象α的实例变量x而由σ得到。 我们也使用τ [y <$→ v]，其中出现在y中的实例变量是不变的; σinst [y <$→ v]和σ [α]。y<$→v]是相似的，其中实例变量是不变的。对于全局状态，σ[α<$→σinst]等于σ，除了在α上;注意，如果α不在σ的域dom（σ）中，则该操作以初始状态σinst将现有对象的集合扩展α。2.2.2操作语义在本节中，我们将介绍异常处理的操作语义（参见见图3）。此外，我们在图2中列出了正常控制流的一些规则;对于其余的转换规则，我们参考[2]。[6]这些限制可以放宽，但会增加证据制度的复杂性。286E. Abraham等人/理论计算机科学电子笔记159（2006）2810Einst0m∈/{start，run，wait，notify，notifyAll}nsyncm（u）{body}∈Methcβ=[[e]]σ（α），τ∈Valc（σ）τ′=τinit[u<$→[[e]]σ（α），τ]0EEC所有Tm（e）;stm）}，σ−→ Tstec{（α，τ，receiveu;stm）<$（β，τ′，body）}，στ′′σ（β），τ′=τ[uret<$→[[eret]]E]返回Tβ=[[e]] σ（α），τ∈Val c（σ） <$started（T <${Val c（α，τ，e. start（）;stm）}，β）Tstart（）;stm）}，σ（α，τ，stm），（β，τinit，body）}，σC全部启动run，crun，c返回运行T图二. 操作语义学（1）程序的初始配置<$T0，σ0<$满足dom（σ0）={α}，σ0（α）=σinit[this<$→α]，T0={（α，τinit，bodyrun，c）}，其中c是主类，α∈Valc.我们称程序的一个构形为可达的，当且仅当它是一个可达的集合T0，σ0−→可达的T，σ0是一个可达的集合T0，σ0是一个可达的集合，且σ0−→可达的X-可达集合T0。允许一种特殊形式的错误处理：如果发生了一些意外或不允许的事情，执行线程可能会抛出一个异常对象。7抛出的异常中断正常控制流，该正常控制流移动到给定类型的“非实时”执行和非实时执行，如下面所解释的通常，try-catch-finally块从左到右执行在try部分中引发的异常将控制转移到第一个匹配的catch子句（如果有的话），这可能会引发自己的异常 finally部分的执行与是否引发异常或是否已将其写入“falle n thr o u g h“无关。如果最后所有的类都使用了hrow，则会删除先前部分的未捕获异常（如果有的话）。在执行try-catch-finally块时，try stm0catch。. . 然而，执行文件夹可能是一种“操作”，例如，G. ，stm′catch. . . 是的。我们也把这样的块称为语句，即使它们不是原始语法中的语句。没有出现这种打开块的语句称为try-closed。在输入try-catch-finally语句后（参见ruleTRY）try子句一直被执行，直到它终止或抛出异常。抛出的异常由处理给定类型异常的第一个catch子句捕获（如果有）。ruleCATCH）;之后，继续执行finally子句7与Java不同，在我们的语言中，所有对象都可以作为异常。E. Abraham等人/理论计算机科学电子笔记159（2006）2812871 1 1 n n n nn+1E1 1 1 n n n nn+1EE在βEββE在出来EETTTβ输出n≥0{\displaystyle {\frac{ . . catch（cnun）stmn最后stmyrt;stm′）}，σ −→最终在Tstm是try-closedstm ′= catch（c u）stm。. . catch（c u）stm finally stmyrt1≤i≤n[[e]]σ（α），τ∈Valc i<$1≤j

下载后可阅读完整内容，剩余1页未读，立即下载