您如何在 Eclipse 中使用 CodePro 的合约？答案

【问题标题】：How do you use CodePro's contracts in Eclipse?您如何在 Eclipse 中使用 CodePro 的合约？
【发布时间】：2011-11-17 03:02:14
【问题描述】：

我以为我了解 CodePro 的合同，但它们似乎没有任何作用。例如：

public class ContractTest {

    private int number;

    /**
     * @pre inputNumber > 0
     * 
     * Alternatively:
     * @post number > 0
     */
    public void setNumber(int inputNumber) {
        number = inputNumber;
    }

    public int getNumber() {
        return number;
    } 

    public static void main(String args[]) {
        ConditionsTest conditionsTest = new ConditionsTest();
        conditionsTest.setNumber(-5);
        System.out.println("Number: " + conditionsTest.getNumber());
    }
}

运行 main(String[]) 方法导致：

number: -5

要打印。没有编译警告（预期），也没有抛出异常。此外，CodePro 生成的 junit 测试方法不受合约影响。

那么您如何使用 CodePro 的合约呢？

【问题讨论】：

不是你的问题的答案，但你知道你可以使用断言来实现同样的事情吗？参见例如 deitel.com/articles/java_tutorials/20060106/Assertions.html 最好的事情是断言是核心 java 的一部分。
断言是运行时，我希望合约是编译时。断言只会在代码运行时提醒程序员，而且通常不是程序的所有路径都可以测试。另外，如果 CodePro 合约类似于 cofaja 合约，那么这些合约可以被继承。
@Mowgli 对于大多数有趣的合约，基本上不可能（我会说无法确定，但我不是 100% 确定那里）在不运行实际代码的情况下确定条件是否成立。然后是输入的问题。因此，我无法想象有任何图书馆试图这样做，因为它只能在玩具示例中使用。（严格来说并不正确，模型检查实际上与此有些相似）
我原以为它会类似于类型检查和静态分析。但我不知道，因为文档很少，我无法让它工作。

标签： java eclipse contracts codepro

【解决方案1】：

您确定应该收到编译警告吗？据我所见，CodePro 中的合约仅用于生成带有正确断言的 JUnit 测试用例，而不是发出警告。

【讨论】：

不，我不确定是否应该收到编译警告。我无法让它工作，而且几乎没有任何文档。但即使为 junit 工作也会非常有用，因为生成的 junit 代码通常会生成无用的测试，这些测试将受益于一点指导。
是的。他们直接与合同相矛盾:(

【解决方案2】：

如果你想在你的 java 开发中包含契约式设计，Cofoja 绝对是一个更好的选择：

http://code.google.com/p/cofoja/

编辑：在 Eclipse 中设置 Cofoja：

http://fsteeg.com/2011/02/07/setting-up-contracts-for-java-in-eclipse/

【讨论】：

我很想使用 Cofaja，但是让它与 eclipse 一起工作很麻烦。
我希望 CodePro 的合同是相似的，因为我认为它们是由同一组开发的（虽然不确定）。
在 Eclipse 中使用 Cofoja：fsteeg.com/2011/02/07/setting-up-contracts-for-java-in-eclipse
谢谢。我看到的上一个指南使它看起来比您的链接更令人生畏。