Java建模语言是否可执行？

我学习软件工程课程，在那里我看到了JML的使用。下面是一段代码示例：Java建模语言是否可执行？

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

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

我的问题是，当我们调用与F = -4这个sqrt函数，这段代码给出错误或抛出一个异常，或给予任何警告？我在我的电脑上试过它，它运行良好并打印出-2。那么这意味着JML是可执行的？为什么我们不使用评论来做到这一点？谁能解释一下？

感谢

来源

2013-05-28 yrazlik

好，这里是代码，我问一些有关的代码。我不明白downvote！ – yrazlik

JML不是Java的一部分。这是一个由研究人员联盟设计的扩展，但没有官方的支持。因此，JML注释不被Java编译器考虑，但你可以编译一个特殊的编译器JML标注的Java程序，使得可执行规范将被考虑在内。例如，JML4C。

来源

2013-05-28 21:43:38

谢谢，这有帮助 – yrazlik

你是不是做的平方根（Math.sqrt(f)，见http://docs.oracle.com/javase/6/docs/api/java/lang/Math.html#sqrt(double)），用2（f/2）划分。所以这没什么不妥。你需要的是使用Math.sqrt（...），如果这是我认为你需要查看你的方法的名称。

来源

2013-05-28 21:37:53

其实在这里并不重要。我只是想知道这一点：我给出了一个函数的前提条件，即参数必须> = 0，但是我用参数<0调用它，它可以工作。如果JML是可执行的，为什么会出现这种情况？为什么没有错误或警告？ – yrazlik

哦，那么在这种情况下，我认为你错过了行末的最后一个';'。 –

那么，这个代码本身不会为你创建的任何警告。存在各种工具，这使得使用JML规格，例如：

jmlrac：执行
ESC/Java2的：静态验证;编译时证明合同未有违反
jmldoc：javadoc样式的文件
jmlc：断言检查编译
jmlunit：单元测试工具

除此之外，JML规范，如果正确使用，向外国读者/代码维护人员展示程序员的意图。

来源

2013-05-28 21:46:19 McMannus

Java建模语言是否可执行？

回答

相关问题