WEB开发网
开发学院WEB开发Jsp JML起步--使用JML改进你的Java程序(3) 阅读

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

 2008-01-05 09:56:18 来源:WEB开发网   
核心提示:请大家回忆一下代码段2中pop()方法的后处理代码:ensureselementsInQueue.equals(((JMLObjectBag) \old(elementsInQueue)) .remove(\result)) &&\result.equals(\old(peek())); 这里我们说有一个副作用,那就是

  请大家回忆一下代码段2中pop()方法的后处理代码:
  
  ensures
  
  elementsInQueue.equals(((JMLObjectBag)
  
         \old(elementsInQueue))
  
                .remove(\result)) &&
  
  \result.equals(\old(peek()));
  
  这里我们说有一个副作用,那就是在从elementsInQueue删除一个元素的时候会有副作用。事实上,这里还可能有其他的副作用。比方说,一个pop()方法的具体实现中假如修改了m_isMinHeap的值,那么就把排序方法从一个小顶堆变成了大顶堆。只要这种修改能够返回正确结果,就不会引起运行期间的断言检查异常,可是这个却事实上削弱了JML行为规范的作用。我们可以加强后置条件,不答应除了修改elementsInQueue以外的任何改变,请看下面的代码:
  
  代码断7  加强的后置条件
  
  ensures
  
  elementsInQueue.equals(((JMLObjectBag)
  
        \old(elementsInQueue))
  
                .remove(\result)) &&
  
  \result.equals(\old(peek())) &&
  
  isMinimumHeap == \old(isMinimumHeap) &&
  
  comparator == \old(comparator);
  
  从中我们可以看出,通过加入形如x == \old(x)的语句,我们可以消除变量x发生改变的副作用。可是有一个问题,假如用这种办法,每一个方法在它的后置条件都要为每一个变量加上这么一句,这样就会导致行为规范的混乱。而且假如我们给一个类增加一个成员的变量的话,那么我们就得在这个类的所有方法的后处理规范中增加一句,这将让维护变得异常困难。 JML通过引入assignable语句提供了一种更好地解决方案。
  
  assignable 语句
  使用assignable语句,我们可以这样完成pop()方法的后置条件:
  
  代码段8  在方法的行为规范中使用assignable语句
  
  /*@
  
    @ public normal_behavior
  
    @  requires ! isEmpty();
  
    @  assignable elementsInQueue;
  
    @  ensures
  
    @   elementsInQueue.equals(((JMLObjectBag)
  
    @     \old(elementsInQueue))
  
    @            .remove(\result)) &&
  
    @   \result.equals(\old(peek()));
  
    @*/
  
  Object pop() throws NoSUChElementException;
  
  只有在assignable语句中列出的变量才能在一个方法的实现中修改。上面pop()方法的assignable语句的意思是在pop()方法的实现中可以修改elementsInQueue的值,除此之外的其他变量,比如isMinimumHeap、comparator等等都不可以修改。假如你在pop()方法的实现中修改了m_isMinHeap的值,那么编译的时候就会产生一个错误。(不过当前的JML编译器尚没有支持这个,也就是没有检查在方法的实现中,是否只修改在assignable语句中指定的变量。)
  
  修改规则
  我们前面说只有在assignable语句中列出的变量才能在一个方法的实现中修改,这其实是有点简化的说法。事实上,假如以下任意一个条件是 true,该规则就答应方法修改一个变量(loc):
  
  assignable语句中显式列出loc 。
  assignable语句中列出的变量依靠于loc。(比如说假如我们声明“assignable isMinimumHeap;” ,因为模型域isMinimumHeap依靠于具体域m_isMinHeap,所以该 assignable语句意味着方法不仅可以修改显式声明的isMinimumHeap,而且还能修改m_isMinHeap。)
  方法开始执行时loc尚没有分配。
  loc 是方法的局部变量或者是方法的形式参数。
  最后一种情况答应一个方法修改它的参数,即使这个参数没有显式地出现在assignable语句中。粗略一看,这个似乎答应一个方法通过参数传递答应它的调用者修改变量的值。比方说,有一个方法foo(Bar obj),它里面有一个语句obj = anotherBar。不过虽然这个语句修改了obj的值,却不会影响到foo()的调用者,因为虽然这两个obj都是指向一个Bar对象,而且具有一样的名字,foo()方法中的此obj实际上与foo()的调用者中的彼obj是不同的(译者注:关于这一点,请参考java中索引与对象的概念)。
  
  现在我们考虑假如方法foo(Bar obj)里面有一个语句obj.x = 17会怎么样?这个将显式地改变调用者中的变量。这是有问题的。assignable 语句的规则答应一个方法不需要在assignable 语句中声明就可以修改传入参数的值,不过它并不答应修改参数的成员变量,具体在这里来说,就是不答应修改obj.x的值。假如你希望在foo()方法中修改obj.x的值,你就必须在assignable 语句中声明,你可以写assignable obj.x; 。
  
  assignable 语句中可以使用两个JML要害字,\nothing和\everything。 我们可以通过assignable \nothing 语句来表明一个方法没有任何副作用;同样,我们可以通过assignable \everything语句来表明我们的方法可以修改一切变量的值。早先我们使用了一个JML要害字pure,它就等同于使用assignable \nothing; 。

Tags:JML 起步 使用

编辑录入:爽爽 [复制链接] [打 印]
赞助商链接