java-如果JML中带有return的if语句

内容导读

互联网集市收集整理的这篇技术教程文章主要介绍了java-如果JML中带有return的if语句，小编现在分享给大家，供广大互联网技能从业者学习和参考。文章包含873字，纯文字阅读大概需要2分钟。

内容图文

我需要设置一个后置条件,以确保如果size_为0,则返回null.

 if(size_ == 0)
  return null;

我如何在JML中做到这一点？有任何想法吗？以下操作无效：

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

提前致谢

解决方法:

尝试

//@ 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：

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.

内容总结

以上是互联网集市为您收集整理的java-如果JML中带有return的if语句全部内容，希望文章能够帮你解决java-如果JML中带有return的if语句所遇到的程序开发问题。 如果觉得互联网集市技术教程内容还不错，欢迎将互联网集市网站推荐给程序员好友。

内容备注

版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 gblab@vip.qq.com 举报，一经查实，本站将立刻删除。

内容手机端