类方法的 JML 后置条件是否可以包含对另一个方法调用的调用
例如我有这个类:
public class A
{
public int doA(x)
{ ... }
public int doB(int x, int y)
{ ... }
}
对于 doB 的后置条件,我可以:确保 doA(x) = doA(y)
?
最佳答案
是的,前提是调用的方法不包含副作用并且声明为纯方法:
The /@ pure @/ comment indicates that peek() is a pure method. A pure method is one that doesn't have side effects. JML only allows assertions to use pure methods. We declare peek() to be pure so it can be used in the postcondition of pop(). If JML allowed non-pure methods in assertions then we could inadvertently write specifications that had side effects. This could result in code that works when compiled with assertion checking enabled but doesn't work when assertion checking is disabled.
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)
{ ... }
}
关于java - JML 后置条件包含类方法调用,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/13602989/