异常行为
前面给出的行为规范要求调用peek() 和 pop()方法时队列不能为空但其实当队列空时是有可能会调用这两个方法的如果发生这种情况这两个方法就会抛出一个NoSuchElementException异常我们必须修正我们前面制定的行为规范允许这种可能的发生在这种情况下我们要使用JML的exceptional_behavior语句
到目前我们的行为规范还是以public normal_behavior打头的这里normal_behavior关键字表示这是一个正常行为方法不会抛出任何异常使用public exceptional_behavior标记可以用来描述抛出异常的行为下面的代码段显示了类PriorityQueue中peek()方法的行为规范中的异常部分
代码段exceptional_behavior标记
/*@
@ public normal_behavior
@ requires ! isEmpty();
@ ensures elementsInQueuehas(\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的疑问并且审阅了你所看到的这篇文章
