JML 中带 return 的 if 语句

发布于 2024-10-06 12:44:57 字数 226 浏览 0 评论 0原文

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

 if(size_ == 0)
  return null;

我如何在 jml 中做到这一点？有什么想法吗？以下不起作用：

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

提前致谢

原文

i need to set up a postcondition which ensures to return null if size_ is 0. Based on

 if(size_ == 0)
  return null;

how can i do that in jml? any ideas? Following doesn't work:

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

thanks in advance

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

又怨 2024-10-13 12:44:57

尝试

//@ 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 \结果
在普通后置条件或非 void 方法的修改目标中，特殊标识符 \result 是一个规范表达式，其类型是该方法的返回类型。它表示该方法返回的值。 \result 仅允许在用于修改非 void 方法的声明的 Ensure、also_ensures、modify 或 Also_modizes 编译指示内。

Try

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

Example:

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

    return size_.length() > 0;
}

You could also simply write it like this:

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

Here is the documentation for \result:

3.2.14 \result
Within a normal postcondition or a modification target of a non-void method, the special identifier \result is a specification expression whose type is the return type of the method. It denotes the value returned by the method. \result is allowed only within an ensures, also_ensures, modifies, or also_modifies pragma that modifies the declaration of a non-void method.

回复收藏 0 原文

拥醉 2024-10-13 12:44:57

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

其次，该方法的返回类型是什么？ 对象还是基元（布尔）？

您不能将基本类型与 null 进行比较，也不能在应该返回基本类型的情况下返回 null。如果我们假设 size_ 是 int 并且返回是 boolean 那么后置条件将是

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

First of all: what type is size_, Object or 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