来自: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(esult);

@ 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专区。


<完>