Java建模语言是否可执行

Question

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

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

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

我的问题是，当我们用f=-4调用这个sqrt函数时，这个代码是否给出错误或抛出异常或给出任何警告?我在我的电脑上试了一下，它工作得很好，打印出了-2。那么JML是可执行的是什么意思呢?为什么我们不直接使用注释呢?有人能解释一下吗?

谢谢

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(…)，如果这是我认为你需要看看你的方法的名称。