JML后置条件包含类的方法调用
问题描述:
一个JML后置条件的一类方法可以包含调用另一个方法调用JML后置条件包含类的方法调用
例如,我有这个类:
public class A
{
public int doA(x)
{ ... }
public int doB(int x, int y)
{ ... }
}
对于DOB的后置条件,我可以有:ensures doA(x) = doA(y)
?
答
是,所提供的称为方法不包括副作用和被声明为纯:
的/ @纯@ /注释指示PEEK()是一个纯方法。纯粹的方法是没有副作用的方法。 JML仅允许 断言使用纯方法。我们声明peek()是纯的,所以它可以在pop()的后置条件中使用 。如果JML允许在断言中使用非纯方法 ,那么我们可能会无意中编写规范,其中 有副作用。这可能导致代码在编译 时启用断言检查,但在断言 检查被禁用时不起作用。
http://www.ibm.com/developerworks/java/library/j-jml/index.html
public class A
{
public /*@ pure @*/ int doA(int x)
{ ... }
//@ requires ...
//@ ensures doA(x) == doA(y)
public int doB(int x, int y)
{ ... }
}