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

Question

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

http://jmlspecs.sourceforge.net/

使用：

• OpenJML
• Netbeans 7.3
• Java SDK 1.7

我已经将 OpenJML jar 文件添加到 Netbeans 的类路径中。我尝试了你简单的 cofoga google jml 版本 导入 com.google.java.contract.Ensures； 导入 com.google.java.contract.Requires 然后你可以添加前置条件和后置条件

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

Answer 1

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

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