Java中基于类型的无限跟踪属性的实现
Type-based Enforcement of Infinitary Trace Properties for Java
摘要：
提高软件质量的一个常用方法是使用编程指南来避免常见的错误。在本文中，我们考虑的问题，执行Featherweight Java（FJ）的准则。我们形式化的指导方针，有限或无限的执行轨迹集，并开发一个基于区域的类型和效果系统FJ，可以执行这样的指导方针。我们建立在Erbatur，Hofmann和Zalberlinescu的工作，谁提出了一个类型系统，用于验证终止FJ程序的有限事件迹。我们完善这个类型系统，分离区域类型从FJ类型，并使用霍夫曼和陈的想法来扩展它，以捕捉无限的痕迹产生的非终止程序。我们的类型和效果系统可以表达有限和无限的痕迹的属性，并可以计算有关FJ程序可能的无限痕迹的信息。具体地说，一个方法的无限迹集被构造为计算方法体的可能迹的算子的最大不动点。我们的类型推断算法是通过工作与有限抽象的系统的基础上Büchi自动机。
英文摘要：
A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. In this paper, we consider the problem of enforcing guidelines for Featherweight Java (FJ). We formalize guidelines as sets of finite or infinite execution traces and develop a region-based type and effect system for FJ that can enforce such guidelines. We build on the work by Erbatur, Hofmann and Zălinescu, who presented a type system for verifying the finite event traces of terminating FJ programs. We refine this type system, separating region typing from FJ typing, and use ideas of Hofmann and Chen to extend it to capture also infinite traces produced by non-terminating programs. Our type and effect system can express properties of both finite and infinite traces and can compute information about the possible infinite traces of FJ programs. Specifically, the set of infinite traces of a method is constructed as the greatest fixed point of the operator which calculates the possible traces of method bodies. Our type inference algorithm is realized by working with the finitary abstraction of the system based on Büchi automata.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
