java - 在 JML 中返回 if 语句

Question

我需要设置一个后置条件，确保在 size_ 为 0 时返回 null。基于

 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
在普通的后置条件或非空方法的修改目标中，特殊标识符 \result 是一个规范表达式，其类型是方法的返回类型。它表示方法返回的值。\result 只允许在修改非 void 方法声明的 ensure、also_ensures、modifies 或 also_modifies 杂注中使用。

Answer 2

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

Secondly, what the return type of the method? Object or primitive(boolean)?

You cannot compare a primitive type to null, or return null where a primitive type is supposed to be returned. If we assume size_ is int and the return is boolean then the the post-condition would be

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