Java 建模语言是否可执行？

Question

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

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

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

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

谢谢

Answer 1

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

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

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

Answer 2

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

Answer 3

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