1

我正在学习软件工程课程，在那里我看到了 JML 的用法。这是一段示例代码：

//@ requires f >= 0.0 
public float sqrt(float f) { 
   return f/2;
}

它说正式的 JML 规范是可执行的！

我的问题是，当我们使用 f=-4 调用这个 sqrt 函数时，这段代码是否给出错误或抛出异常或给出任何警告？我在我的电脑上试了一下，效果很好，打印出-2。那么JML可执行是什么意思呢？为什么我们不只使用评论来做到这一点？谁能解释一下？

谢谢

4

3 回答 3

2

好吧，这段代码本身不会为您创建任何警告。存在多种使用 JML 规范的工具，例如：

  • jmlrac：测试执行期间是否违反断言
  • ESC/Java2：静态验证；编译时证明合约从不违反
  • jmldoc：javadoc 风格的文档
  • jmlc：断言检查编译器
  • jmlunit：单元测试工具

除此之外，如果使用得当，JML 规范会向外国读者/代码维护者揭示程序员的意图。

于 2013-05-28T21:46:19.420 回答
1

您不是在做平方根（Math.sqrt(f)，请参阅http://docs.oracle.com/javase/6/docs/api/java/lang/Math.html#sqrt(double)），而是除以 2（f/2）。所以这并没有错。你需要的是使用 Math.sqrt(...) 如果这是我假设你需要查看你的方法的名称。

于 2013-05-28T21:37:53.313 回答
1

JML 不是 Java 的一部分。它是由研究人员联盟设计的扩展，但未经官方认可。因此，Java 编译器不会考虑 JML 注释，但您可以使用特殊编译器编译带有 JML 注释的 Java 程序，以便将可执行规范考虑在内。例如，JML4C。

于 2013-05-28T21:43:38.237 回答