如何将JML (openJML)应用于Java代码？

Question

如何将JML应用于Java代码？我仍然是新的设计合同，并相当迷失如何将它应用于程序。

http://jmlspecs.sourceforge.net/

使用：

• OpenJML
• Netbeans 7.3
• JavaSDK1.7

我已经将OpenJML jar文件添加到Netbeans的类路径中。我尝试过cofoga版本，您只需导入com.google.java.contract.Ensures；导入com.google.java.contract.Requires，然后就可以添加前和后条件。

如何在我的程序中使用openJML指定前置条件和post条件？

Answer 1

我找到了所需的内容；正在导入带有注释的库：

import org.jmlspecs.annotation.Requires;
import org.jmlspecs.annotation.Ensures;