我正在学习软件工程课程，在那里看到了JML的用法。这是一个示例代码：
//@ requires f >= 0.0
public float sqrt(float f) {
return f/2;
}
它说正式的JML规范是可执行的！
我的问题是，当我们用f = -4调用此sqrt函数时，此代码是否给出错误或引发异常或给出任何警告？我在计算机上尝试了一下，效果很好，并打印了-2。那么，JML是可执行的意味着什么？为什么我们不仅仅使用注释来做到这一点？谁能解释？
谢谢
最佳答案
JML不是Java的一部分。它是由研究人员联盟设计的扩展，但未经官方认可。这样，Java编译器不会考虑JML注释，但是您可以使用特殊的编译器来编译带有JML注释的Java程序，以便将可执行文件规范考虑在内。例如，JML4C。