JML起步---使用JML 改进你的Java程序(4)

内容: 来自:http://www-106.ibm.com/ 作者:Joe Verzulli 异常行为前面给出的行为规范要求调用peek() 和 pop()方法时队列不能为空，但其实当队列空时是有可能会调用这两个方法的。如果发生这种情况，这两个方法就会抛出一个NoSuchElementException.异常。我们必须修正我们前面制定的行为规范，允许这种可能的发生。在这种情况下，我们要使用JML的exceptional_behavior语句。 到目前，我们的行为规范还是以public normal_behavior打头的。这里normal_behavior关键字表示这是一个正常行为，方法不会抛出任何异常。使用public exceptional_behavior标记可以用来描述抛出异常的行为。下面的代码段显示了类PriorityQueue中peek()方法的行为规范中的异常部分： 代码段9 exceptional_behavior标记 /*@ @ public normal_behavior @ requires ! isEmpty(); @ ensures elementsInQueue.has(result); @ also @ public exceptional_behavior @ requires isEmpty(); @ signals (Exception e) e instanceof NoSuchElementException; @*//*@ pure @*/ Object peek() throws NoSuchElementException; 像我们前面看到的所有例子一样，这个规范的第一部分也是以public normal_behavior开头，表示正常行为；不同的是，这个规范还有第二部分，以public exceptional_behavior开头，描述了异常行为。与normal_behavior 语句一样， exceptional_behavior 语句也有一个 requires 语句。这个requires 语句表示当抛出signals 语句中所列的异常时必须满足的条件。在上面的例子中，如果isEmpty()方法返回真的话，peek()就会抛出一个NoSuchElementException异常。 signals 语句signals 语句是形如signals(E e) R的语句，其中E是Exception类本身或其一个子类，R是一个表达式。JML 用如下方式解释一个signal 语句：如果有一个类型为E的异常抛出的话，就检查是否为R真。如果是，就执行既定规范；否则，抛出一个unchecked exception（译者注：unchecked exception又叫做RuntimeException，关于这两个概念，请参考Java语言中关于异常的描述），用以表示我们的程序代码违背了exceptional_behavior规范的要求。 上面peek()方法中的signals语句的意思是如果队列为空，就抛出一个NoSuchElementException异常。如果peek()方法在运行中抛出不是NoSuchElementException的其它异常的话，那么JML就会把这当成一个错误，因为e instanceof NoSuchElementException不是true。如果你既想处理NoSuchElementException异常又想处理其它运行期异常，我们可以修改上面的signals语句，改为signals (NoSuchElementException e) true; 。这个意思是说，如果peek()方法抛出一个NoSuchElementException异常的话，那条件true必须为真，而true是一个常量，总是可以满足条件，所以对于NoSuchElementException异常的处理可以正常进行。不过我们这里并没有提及关于其它异常的信息，而peek()方法可以抛出它的签名（译者注：方法的签名是指，方法声明的各个部分，具体来说，是方法名称、参数类型、返回类型和抛出异常的总称）允许的任何异常。它的签名说它可以抛出NoSuchElementException异常，这就意味着它既可以抛出NoSuchElementException异常，又可以抛出RuntimeException。 如果队列中存在一些元素而且当我们调用peek()方法时还是抛出一个NoSuchElementException异常（或者其他异常），JML运行期断言检查就会抛出一个unchecked exception，这表示正常的后置条件失败。 结论本文简单介绍了JML的概念，说明了它对面向对象系统的分析和设计的贡献，通过实例演示了如何在Java程序中使用JML标记。你可以从下面所列的资源中下载本文中所使用的完整的代码，还可以从中找到更多的关于JML的信息。 你可以使用开源的JML编译器来编译你含有JML标记的代码，所生成的类文件会在运行时自动检查JML规范。如果你的程序没有实现规范中规定的事情，JML就会抛出一个unchecked exception 来说明你的程序违背了哪一条规范。这可以帮助我们捕获程序中的bug，而且能保证我们的代码与文档（JML格式的文档）高度一致。 JML运行期断言检查编译器是第一个JML工具，其他相关工具还有jmldoc和jmlunit等等。Jmldoc与javadoc工具相似，不同的是它在生成的HTML格式文档中包含JML规范；jmlunit可以成生一个Java类文件测试的框架，它可以让你很方便地使用JUnit工具测试含有JML标记的Java代码。你还可以从下面所列的资源中找到其他关于JML各个方面的相关内容。 在此请允许我向 Gary Leavens 和 Yoonsik Cheon表示深深的谢意，是他们帮我解决了一部分关于JML的疑问并且审阅了你所看到的这篇文章。 资源 下载本文中所用的源代码 。 Sourceforge是JML规范、开源JML工具如JML编译器、jmldoc、jmlunit以及相关信息的主页。 PriorityQueue 接口和 BinaryHeap 类是开源项目 雅加达通用集合组件（JCCC）的一部分。 Gary T. Leavens、Albert L. Baker和Clyde Ruby的 'JML设计起步' (爱荷华州立大学计算机科学系，2003年1月) 是对JML的更为详细地介绍。 Bertrand Meyer在面向对象软件构造，第二版一书中关于通过契约（JML最基本的概念）进行设计的讨论(Prentice Hall, 1997)。 Granville Miller在介绍面向对象系统建模中关于 Java建模 部分（developerWorks, 2002）。 Eric Allen在'Diagnosing Java code: Assertions and temporal logic in Java programming' (developerWorks, July 2002)一书中讨论了一些断言检查限制的问题。 Kyle Brown在'A stepped approach to J2EE testing with SDAO' (developerWorks, March 2003)一文中讨论了如何把模拟数据对象与分层测试联合起来。 Java程序设计的各个方面的信息请参考IBM developerWorks Java专区。 Java, java, J2SE, j2se, J2EE, j2ee, J2ME, j2me, ejb, ejb3, JBOSS, jboss, spring, hibernate, jdo, struts, webwork, ajax, AJAX, mysql, MySQL, Oracle, Weblogic, Websphere, scjp, scjd