如果在JML中带有返回的语句

Question

我需要设置一个后条件，该条件确保返回null如果size _ 0.

 if(size_ == 0)
  return null;

我该如何在JML中这样做？有任何想法吗？以下无效：

//@ ensures size_ == null ==> \return true;

提前致谢

Answer 1

尝试

//@ ensures size_ == null ==> \result == true;

例子：

//@ ensures size_ == null ==> \result == true;
public boolean sizeUndefined() {
    if (size_ == null)
        return true;

    return size_.length() > 0;
}

您也可以简单地这样写：

//@ ensures size_ == null ==> \result;

这是 文档 \result:

3.2.14 \result
在普通的后条件或非空隙方法的修改目标中，特殊标识符结果是规范表达式，其类型是该方法的返回类型。它表示该方法返回的值。 结果仅在确保，_senter，修改或编码的pragma中允许结果，以修改非流动方法的声明。

Answer 2

首先：什么类型是 size_, Object 或者 primitive(int)?

其次，该方法的返回类型是什么？ Object 或者 primitive(boolean)?

您不能将原始类型与 null, ，或返回 null 应该返回原始类型的地方。如果我们假设 size_ 是 int 回报是 boolean 那么后的条件将是

//@ ensures size_ == 0 ==> \result;