理论计算机科学电子笔记157（2006）119-132www.elsevier.com/locate/entcs用扩展的静态检查提高基于Web的企业应用程序的质量：一个案例研究FR'ed'ericRioux1，PatriceChalin1计算机科学与软件工程Concordia University墨西哥城摘要ESC/Java 2是一个静态检测Java程序中错误的工具，它使用Java建模语言（JML）作为其注释语言。ESC/Java 2可以模块化地推理基于Java Web的企业应用程序（WEA）的代码，并发现潜在的错误。在本文中，我们评估了ESC/Java 2通过检测设计和实现问题来帮助开发人员提高WEA质量的有效性。关键词：基于Web的企业应用，扩展静态检查，契约式设计，Java建模语言1引言编程语言的发展使软件工程师能够开发越来越大的软件系统，同时保持或提高产品质量。 这已经部分地通过增加语言的抽象级别、利用新的范例（诸如面向对象）以及使得编译器能够执行静态检查和/或在前者既不可能也不实际时嵌入运行时检查代码来实现。鉴于上述情况，有人可能会问：下一个编程语言将是什么？1电子邮件：{f rioux，chalin}@ cse.concordia.ca1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.050120F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119和工具的进步，这些进步很可能成为主流？我们认为，对于大多数应用领 域 ， 这 些 进 展 可 能 包 括 按 合 同 设 计 （ DBC ） 和 扩 展 静 态 检 查（ESC）。DBC可以作为一种轻量级的形式化方法逐渐集成到项目中，使开发人员能够习惯这种方法。除其他外，lint-like [7] ESC工具— 许多程序员都很熟悉，然后可以使用这些额外的正式文档来执行快速有效的检查。企业应用程序（EA）的特点通常是它们操作的数据量大，它们嵌入的业务规则，以及它们需要与其他（通常是遗留的）应用程序集成[6]。电子商务的一个重要类别是基于网络的企业应用程序（WEA），企业和消费者越来越多地使用这些应用程序-仅在2004年第三季度，美国的零售电子商务销售额估计为176亿美元，比上一季度增长4.7%。这一数字自1999年以来一直在上升[16]。本文介绍了一个案例研究的初步结果，其主要目标是评估ESC/Java 2[1][2][4]在帮助开发人员通过检测设计和实现问题来提高WEA质量方面的有效性。在这样做的过程中，我们为一些javax和java.sql类编写了轻量级的JML规范我们研究的主题是一系列主要基于一个小框架（名为SoenEA）的WEA，该框架已在Concordia使用了近两年，现在正在教授WEA架构和设计的课程。本文的组织结构如下。DBC、ESC和ESC/Java 2在第2节中介绍。第3节重申了我们的目标，并提出了案例研究，包括解释我们选择的应用领域。其余部分讨论了案例研究的结果、未来的工作和结论。2背景2.1契约式设计（DBC）DBC是一种查看两个类之间关系的设计方法— 供应商和客户-作为正式协议或合同[12]。这种协议表明了各方契约通常采用前置条件、后置条件和不变量的形式合约是模块规范的一种形式。我们相信，如果他们的合同是明确的，正确的和可验证的，那么就有可能提高我们对大型复杂系统的信任水平。DBC目前由Eiffel编程语言和一些特定语言支持，包括F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119121//@ requires y >= 0;public int findDuplicate（int findDuplicate）{...}Fig. 1.轻量级规范示例行为接口规范语言（Behavioral Interface Specification Languages，BISL）BISL是一种可用于准确描述模块接口的语言，因此，通过定义，实现了DBC。BISL的主要特点是它是为特定的编程语言量身定制的。BISL是一种有趣的规范化语言，因为它们可以用于弥合软件开发生命周期的规范化和设计活动之间的差距它们还为强大的自动验证奠定了基础。此外，它们是可伸缩的，允许根据需要将它们逐步引入到新的开发以及遗留代码中。Java建模语言（JML）是一种Java BISL，由一个国际研究团队积极开发，他们在语言定义和工具实现方面进行了合作。有关最新工具和应用程序的详细信息，请参见[1]。在[8]中描述了JML在DBC中的使用。JML规范可以嵌入Java源文件中，作为专门的for-marted注释或外部规范文件。JML表达式看起来像Java表达式，因为JML保留了Java的大部分Java和JML之间的这种紧密耦合降低了开发人员学习和使用JML所需的负担。JML支持轻量级和重量级规范。轻量级规范没有重量级规范那么详细和完整，通常由单独的子句组成，只描述预期行为的一个方面。JML被设计为支持轻量级规范，并且具有允许省略大多数子句的语义在JML中，方法规范通常写在方法之前。前置条件由requires子句表示，后置条件由ensure子句表示。每个子句都是布尔表达式。方法调用可以在规范中使用，但它们必须是对声明为pure的方法的调用，他们没有一个人，没有一个人。图1和图2分别显示了整数平方根函数的部分和更详细的特性在第一种情况下，唯一的约束是数字必须是正整数;然而，在后一种情况下，函数也保证返回一个在[-y，y]范围内的数字，其平方小于或等于y，其绝对值的平方增加1大于y。122F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119/*@ publicnormal_behavior@需要y >= 0;@确保-y = \result@\result= y@\result * \result = y@y（Math.abs（\result）+ 1）@*（Math.abs（\result）+ 1）; @*/public int findDuplicate（int findDuplicate）{...}图二. 样品重量规格2.2扩展静态检查（ESC）虽然运行时检查代码对于检测和报告错误肯定是有用的，但它给开发人员留下了在运行时处理错误的问题。在可能的情况下，最好能够首先防止这些错误发生。此外，越早发现错误，纠正错误的成本就越低。静态程序检查器允许我们通过静态程序分析来检测这些运行时错误存在各种各样的静态检查工具，从简单的类型检查器到正式的程序验证器。扩展静态检查器是一种特殊的工具，根据[11]，从给定的程序中生成验证条件和逻辑公式，并将它们传递给自动定理证明器。ESC工具的理想特性是完整性和可靠性，即，捕获所有错误，并且不触发假警报（通过在没有错误的地方报告错误）。从工程角度来看，ESC不需要这些特性，特别是因为满足这些特性意味着过度规范和降低检查器的性能[11][5]。ESC工具在出现错误或代码未实现其规范时警告用户。默认情况下，假设了平凡的规范。一个平凡的指定意味着没有特殊的先决条件，执行可能有任何副作用，并且不应该期望特定的后置条件。如果显式编写，默认规范将如图3所示[9]。误报可能表明规范太弱，需要加强。为了实现这样的强化，程序员需要使用工具的注释语言（在代码中以注释的形式出现）来记录设计决策根据Flanagan等人的研究，F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119123/*@ behavior@需要true;@ assignable\everything; @确保true;@signals（Exception）true;@.@*/图三. 默认（即隐式）方法规范再加上未注释的代码会生成过多的警告，这可能会将效益/效益比降低到主流程序员可接受的范围以下[5]。2.3ESC/Java2ESC/Java是一个用于Java的ESC工具，是在ESC/Modula-3工具之后开发的。这两个ESC工具积累了超过12年的经验，并已成功应用于数万行代码[11]。即使ESC/Java使用了复杂的程序验证技术，对于程序员来说，它看起来就像一个简单的类型检查器。此外，由于它执行模块化检查（而不是整个程序检查），因此复杂度可以保持在最低水平[2]。ESC/Java 2将JML作为其注释语言。重型和轻型规格均可接受。像它的前身一样，ESC/Java 2既不健全也不完整。通过使用规范语言中的短语作为ESC注释语言将ESC与JML耦合意味着设计决策使用丰富的语言记录，并且这些规范可以重用，扩展并传递给其他JML工具-例如运行时断言检查编译器JML RAC和正式程序验证工具LOOP [1]。此外，这样的注释语言可以利用Java库的JML规范，以便更好地解释它正在检查的代码JML的一个重要特性是它采用了行为子类型语义[9]，其中子类中重写的方法需要保留其对应超类方法的契约[3]。在下一节中，我们将提到我们认为行为子类型可以如何发挥优势。2.4Java Web企业应用程序（WEA）大多数企业应用程序（EA）都涉及大量的持久性数据。通常，数据库用于存储和访问这些数据。EA的另一个特点是大量的用户交互屏幕。为124F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119Fowler建议使用常见的三层方案，该方案将域逻辑（也称为业务逻辑）与表示和数据源隔离开来[6]。Java WEA的一个有趣的方面是，它们中的大多数使用相同的一小组外部库、超类和接口进行用户交互（例如servlets.jar）和数据库访问（例如java.sql *）。）的。由于JML的行为子类型语义，我们相信在这种情况下，指定常用的超类和接口的投资应该减少指定子类所需的时间，并降低虚警的数量，从而允许开发人员更容易地识别潜在的错误。3为例3.1目标和方法我们案例研究的主要目标是评估ESC/Java 2在帮助开发人员通过检测设计和实现错误来提高软件质量方面的有效性我们早期的决定之一是关于应用领域的选择。我们选择了WEA，因为它是Java开发中最活跃的领域之一。SoenEA是一个小型的WEA框架，在过去的两年中开发出来，用于Concordia大学的软件架构和设计课程。SoenEA包装了代码，例如数据库连接和servlet接口，这样学生就可以在没有全面知识的情况下轻松使用它们这些技术的。该框架还附带了应用程序示例。我们的研究有两个阶段。 在第一阶段，我们将ESC/Java 2应用于SoenEA核心和使用SoenEA的示例应用程序。我们将此包称为A1。第一阶段的目的是：• 获得使用ESC/Java 2的经验，同时• 逐步开发以下规格：· A1应用· SoenEA核心类· A1使用的javax和java.sql包模块。ESC/Java 2执行模块化检查[5][2]，从而允许我们在一次一个A1文件。这是非常有用的，因为ESC/Java 2最初报告了A1的数百个错误。A1包含2.1K行代码（行），或1.6K源代码行（行）。第二阶段的目的是测量由于使用第一阶段开发的SoenEA核心、javax、java.sql模块的注释版本而除了A1包，我们还分析了另外两个F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119125应用程序总计7.6K字节（或5K字节）。我们将把后者称为A3一揽子计划。3.2一般结果这两个阶段需要大约4人-周的外勤人员（全职）。在第一阶段结束时，我们创建了• A1包的注释版本（即SoenEA核心和A1应用程序）。总的来说，由于注释（即，大约100磅）。• javax和java.sql包模块的轻量级规范- 90个子网（379个子网）。这些轻量级规范主要由关于类属性和方法参数的注释组成，限制它们为非空。在第二阶段，使用创建的规范，与使用没有规范的ESC/Java 2相比，A1和A3在下面的小节中，我们将介绍我们在指定外部库（javax和java.sql）以及SoenEA核心方面的一些经验这些材料提出了越来越复杂的问题（在某种程度上，模仿我们通常不得不处理它们的顺序）。最后一小节涵盖了ESC/Java 2为A1包报告的最有趣的错误。在讨论ESC/Java 2发现的错误数量之前，提供我们对“错误”的定义是至关重要的。通过“错误”，我们指的是与方法（或一般来说，类）的预期用途有关的错误。方法的预期用途是其质量标准中记录的内容。如果没有明确的文档说明，则假定默认的隐式说明。当代码不满足规范时，就会发生“故障”。根据DBC，这可能是因为客户端在方法的前置条件未满足时调用方法，或者当方法返回且其后置条件未满足时调用方法。 由于缺少显式规范而导致的误报将被视为故障并命名为 一个“特定的错误”。外部库的错误警报表示ESC/Java 2中缺少规范，而用户模块的错误警报表示真正的具体故障。3.3javax、java.sql和SoenEA核心ESC/Java 2使用代码或规范文件中的JML注释执行静态检查和推理。在没有具体说明的情况下（如126F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119soenEA.applications.assignment.a3.ts.TaskTDG：findAll（）..\ soenEA\applications\assignment\a3\ts\TaskTDG.java：35：警告：可能为 空解引用（NULL）return dbStatement. execute（）;^[0.19 s 10054064字节]失败见图4。 样本假警报/规格故障public class Uncategorized{...public static ResultSet findAll（）抛出Exception，SQLException {Connection db = DbRegistry.getDbConnection（）;PreparedStatement dbStatement =db. tagreStatement（“SELECT * from“+ TABLE_NAME）;return dbStatement.executeQuery（）;//第35}...}图五. TaskTDG代码摘录在第一阶段开始时，javax类的方法就是这种情况）ESC/Java 2假定了默认的规范（第2.2节），这是非常宽容的，很少令人满意。这意味着在没有规范的情况下，ESC/Java 2可能会触发警告，其中许多可能是错误警报或规范故障。（值得庆幸的是，ESC/Java 2为最常见的Java类提供了JML规范，例如，在简单的System.out情况下，这可以防止它警告可能的null解引用。ESC/Java 2在早期阶段报告的特定故障示例I在图4中给出。图5中给出了相应的代码。ESC/Java 2报告变量dbStatement可能在第35行中的指定点为null。 这是不可能的，因为这个变量被设置为db. residedStatement（）的返回值，它总是返回一个对象的引用[15]。这是一个错误的警报，因为没有明确地指定maskedState- ment（）。修复这个错误警报很简单：我们为方法创建一个显式的规范，声明它不返回null结果-参见图6。大部分F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119127java.sql;public interface Connection {//@确保\result！= 无效;public PreparedStatement String s（String s）抛出SQLException;}见图6。 为Connection. BulleredStatement（）为javax和java.sql模块创建的规范，其性质如下：即指定参数和/或返回的结果不为空。ESC/Java 2能够对更多的属性进行静态检查，但是静态检测所有可能的空引用被认为对于案例研究的这个迭代是足够的。与外部库的规范一样，添加到SoenEA核心的大多数注释都具有相同的轻量级性质。这让我们发现了一些非常有趣的错误，我们将在下一节中报告。4具体设计和实施缺陷在本节中，我们报告了在我们研究的第二阶段，A1包中ESC/Java 2发现的最有趣的错误ESC/Java 2报告了A1软件包的102个故障。在识别出的102个故障中，90%是特定故障，即由于缺乏设计文档/规范。通过以方法API规范的形式编写设计文档，可以消除此类错误。下面介绍的故障取自剩余的10%故障。4.1不完全传播的设计变更至少有两个故障是不完全传播的设计变更的表现。例如，在A1应用程序中，一个表示任务的域逻辑类经历了以下设计更改：最初类字段通过setter初始化;随后决定所有字段都通过（非默认）类构造函数初始化。此设计更改的结果是引用类型的类构造函数参数不能再为null。这样的事实已经在Task类中得到了适当的记录，但不是所有的构造函数调用128F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119public class User{ private long id;private String loginId;private String name;private List originatedTasks;private String password;public boolean alert（Object）{如果（obj == null||！(obj return false;User other =（User）obj;return this.id == other.id&&this.loginId.equals（other.loginId）this.name.equals（other.name）this.password.equals（other.password）;}}见图7。 用户类摘录尊重这些限制，或者是因为：• 并不是所有的客户端类都被适当地更新，或者，正如经常发生的那样，• 在应用程序的后续更新中，开发人员仍然依赖于旧的API语义。这两个场景展示了正式记录设计决策和使用扩展静态检查的优势另一个类似的例子发生在SoenEA数据库注册表中。类的初始版本试图强制连接字段永远不会为null。然而，人们意识到这是不可行的。 有趣的是，如果ESC/Java 2在更早的时候使用，这个设计错误从一开始就被发现了。这个类被重新设计了，但是ESC/Java 2帮助发现了一些设计者没有预料到的情况，连接字段仍然可以为空。4.2可能违反行为子类型在 User 类 中 定 义 了 一 个 名 为 equals 的 方 法 （ 图 7 ） ， 从 而 覆 盖 了ObjectESC/Java 2报告说，超类规范（即，Object.equals（）的指定可能不适用于User.equals。最初认为这个错误的原因是User.equals只比较了它的五个属性中的四个但是，在与设计师讨论F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119129soenEA.general.app.Servlet：forwardAbsolute（java.lang.String，javax.servlet.http.HttpServletRequest，javax.servlet.http.HttpServletResponse）.soenEA/general/app/Servlet.java：109：警告：可能为空的解引用（NULL）dispatcher.forward（request，response）;^见图8。 调度程序错误public void forwardAbsolute（String target，HttpServletRequest request，HttpServletResponseresponse）抛出ServletException，java.io.IOException{System. out. println（）; System. out. println（）;return（request，response）;}见图9。 Servlet类摘录人们意识到这是故意的。 因此，为了避免混淆，决定适当的纠正措施是将User.equals重命名为用户.相似这个例子说明了行为子类型化的力量：精心编写的超类规范允许ESC/Java 2发现语义错误。4.3未校验调度程序ESC/Java 2检测到SoenEA核心中的一个错误，我们已经知道，这显然是新手WEA开发人员常见的问题（图8）。框架假设servlet分派器总是初始化的。 事实并非如此[14]。ESC/Java 2 对此事件提供 了警告（基于getRequestDispatcher的默认隐式指定，在本例中是正确的）。故障代码如图9所示。4.4遗漏异常条件数据库连接信息（例如登录ID、密码）记录在SoenEA框架读取的属性文件中。虽然文件不存在的情况得到妥善处理，但文件不包含所需属性的情况没有得到妥善处理。这在代码审查和测试期间都没有发现。130F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）1194.5其他故障剩下的几个错误是简单的可能的空指针取消引用。这方面的一个例子发生在最近添加到框架中的一个文件ESC/Java 2在其中检测到三个可能的空指针取消引用。只有广泛使用框架才能捕获这些，因为该类是一个异常适配器，只在异常情况下使用。5结论我们相信编写JML规范并使用ESC/Java 2验证它们与代码之间的匹配在这个案例研究中花费的时间不仅使我们能够识别和纠正设计问题，而且还迫使我们思考和记录以前做出的设计决策。此外，该工具可以自动验证这些文档我们已经提高了对框架的信任程度，并且通过强制执行行为子类型，我们认为框架是一个更好的重用和扩展候选者。在这个案例研究中，ESC/Java 2证明了自己对WEAs的有用性。然而，它是一个通用的工具，不限于特定的领域的应用。ESC/Java 2的使用可能会扩展到其他应用领域。据我们所知，这个案例研究是第一个涉及ESC/Java 2和WEA域的案例。也许JML在那个特定领域的一个缺点是它目前不支持关于并发的推理。然而，最近有一项提案提出来解决这个问题[13]。尽管如此，我们必须为javax和java.sql编写的轻量级JML规范可以被JML社区重用或补充，并且可以使JML及其支持工具（如ESC/Java 2）更方便Java开发人员使用。我们的案例研究涉及一个相对较小的框架和应用程序，但由于它执行模块化检查，我们相信ESC/Java 2将扩展到更大的应用程序。对于本案例研究，我们使用了ESC/Java 2的最新开发版本（2004年12月）。它被认为是在一个后期的阿尔法周期。因此，我们确实遇到了工具的错误，但没有一个是不能解决的。事实上，当工具失败时，首席开发人员对我们的问题报告和帮助请求当然，创建规范是有成本的。由于这是我们第一个涉及ESC/Java 2的案例研究，因此我们的任务的一个重要部分是致力于学习该工具以及最适合它的JML规范几次假警报也F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119131由于缺少javax和java.sql类的规范。而且，到目前为止，ESC/Java 2还没有集成到任何IDE中。我们有信心，随着研究的进展和ESC/Java 2变得更加成熟和易于使用，成本/收益比将变得越来越有吸引力。6今后工作现在已经指定了一些javax和java.sql类，在未来，我们想再次对其他WEA进行这项研究，看看注释负担是否已经显著降低。由于SoenEA框架每年都有一百多名学生使用，我们计划向他们提供框架的注释版本，并验证他们是否认为使用ESC/Java 2可以提高他们的WEA质量，并帮助他们识别和纠正错误。另一个有趣的途径是重用带注释的SoenEA框架，将其他JML兼容工具应用于它，然后检查有多少编写的规范可以重用，以及WEA开发人员可以从中获得什么好处7确认作者要感谢Daniel Sinnig、Stuart Thiel和匿名评论者提供的宝贵反馈，以及David Cok和Joseph Kiniry帮助我们使用ESC/Java 2并回答我们所有的问题。引用[1] 伯蒂湖，Y. Cheon，D. Cok，M. Ernst，J. Kiniry，G. T. Leavens，K. R. M. Leino和E. Poll，Anoverview of JML tools and applications ， International Journal on Software Tools forTechnology Transfer（STTT）（2004），即将出版。URLftp://ftp.cs.iastate.edu/pub/leavens/JML/sttt04.pdf[2] Cok，D.R. 和j.R. Kiniry，ESC/java2：Uniting esc/java and jml，in：Construction andAnalysis of Safe，Secure，and Interoperable Smart Devices（2004），pp.108比128[3] Dhara ， K.K. 和 G.T. Leavens ， Forcingbehavioralsubtypingthroughspecificationinheritance ， Technical Report 95-20c ， Department of Computer Science ， Iowa StateUniversity，Ames，Iowa，50011（1995）。URLftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.gz[4] Esc/java2.URLwww.sos.cs.ru.nl/research/escjava/[5] 弗拉纳根角，K. R. M.莱诺湖利利布里奇湾Nelson，J. B. Saxe和R. Stata，Extended staticchecking for Java，ACM SIGPLAN Notices37（2002），pp.234-245.[6] Fowler，M.，《企业应用程序架构模式》，Addison Wesley，2002年。 [7]约翰逊，S.，Lint，a c program checker（1978）.URLciteseer.ist.psu.edu/johnson78lint.html132F. Rioux，P.Chalin/理论计算机科学电子笔记157（2006）119[8] Leavens，G.和Y. Cheon，Design by Contract with JML（2003）。URLciteseer.lcs.mit.edu/leavens03design.html[9] Leavens，G. T.，A. L. Baker和C. Ruby，JML的初步设计：Java的行为接口规范语言，技术报告98- 06 y，爱荷华州立大学计算机科学系（2004），见www.jmlspecs.org。URLftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz[10] Leavens，G. T.，K. R. M. Leino，E.波尔角鲁比和B. Jacobs，JML：Notations and ToolsSupporting Detailed Design in Java ， in ： OOPSLA 2000 Companion ， Minneapolis ，Minnesota，ACM，2000，pp.105-106URLftp://ftp.cs.iastate.edu/pub/techreports/TR00-15/TR.ps.gz[11] Leino，K. R. M.，扩展的静态检查：十年展望，计算机科学讲义2000（2001），页。157-？？URLhttp://link.springer-ny.com/link/service/series/0558/bibs/2000/20000157.htm[12] 迈耶湾，“Object-Oriented Software Construction,” Prentice-Hall, Englewood Cliffs, 1997,网址http://www.prenhall.com/allbooks/ptr 0136291554.html[13] Rodr'ıguez，E. ，M. B. D wyer，C. Fla n agan，J. 你好G T. LeavensandRoby，用于多线程程序的模块化规范和验证的扩展顺序规范技术，技术报告SAnToS-TR 2004 -10，堪萨斯州立大学计算和信息科学系（2004年），将出现在ECOOP 2005中。URLhttp://spex.projects.cis.ksu.edu/papers/SAnToS-TR2004-10.pdf[14] Sun java servlet api文档。URLjava.sun.com/j2ee/1.4/docs/api/javax/servlet/package-summary.html[15] Sun java sql api文档。URLjava.sun.com/j2se/1.4.2/docs/api/java/sql/package-summary.html[16] 2004年第三季度电子商务季度零售额。网址www.census.gov/mrts/www/data/html/3q2004.html
我的内容管理
展开
