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

Question

我们如何将JML应用于Java代码？我还是合同设计的新手，不知道如何将其应用到程序中。

http://jmlspecs.sourceforge.net/

使用：

• OpenJML
• Netbeans 7.3
• Java SDK 1.7

我已经将OpenJMLjar文件添加到Netbeans的类路径中。我尝试了cofoga-google-jml版本，您只需导入com.google.java.contrract.Ensure；导入com.google.java.contrract.Requires然后你可以添加前条件和后条件

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

Answer 1

我找到了需要的东西；正在导入带有注释的库：

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