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

2019-08-16 07:36:56来源: 阅读 ()

新老客户大回馈,云服务器低至5折

内容: 来自: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

标签:

版权申明:本站文章部分自网络,如有侵权,请联系:west999com@outlook.com
特别注意:本站所有转载文章言论不代表本站观点,本站所提供的摄影照片,插画,设计作品,如需使用,请与原作者联系,版权归原作者所有

上一篇:运用加密技术保护Java源代码(2)

下一篇:运用加密技术保护Java源代码(1)