在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;

这是the documentation for \result

\result

3.2.14

在正常的后置条件或非void方法的修改目标中，特殊标识符\result是一个规范表达式，其类型是该方法的返回类型。它表示该方法返回的值。\result仅允许在修改非also_ensures方法声明的ensures、also_modifies、modifies或void杂注中使用。

Answer 2

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

其次，方法的返回类型是什么？Object还是primitive(boolean)？

不能将基元类型与null进行比较，也不能在应该返回基元类型的地方返回null。如果我们假设size_为int，返回为boolean，那么后置条件将为

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