带有断言的部分合同设计

Question

我想就合同设计的部分实施的想法获得一些意见。 目标是在不需要外部库的情况下向不提供轻量级合约（仅不变量和后置条件）的语言添加。

我的示例是用 Java 编写的，但我认为这个想法适用于许多 OO 语言。

我们有一个这样的类：

class myClass{
    type1 field1;
    type2 field2;

    public myClass(type1 param1){
        //do something
    }

    public type3 method1(type1 param1, type3 param2){
        if (paramsAreNotOk()){
            throw new IllegalArgumentException();
        }
        // do a lot of things
        return //do something
    }
}

我们这样扩展上面的代码：

class myClass{
    type1 field1;
    type2 field2;

    public myClass(type1 param1){
        //do something

        assert invariant();
    }

    public type3 method1(final type1 param1, final type3 param2){
        assert invariant();
        myClass old;
        assert ((old = this.clone()) != null)

        if (paramsAreNotOk()){
            throw new IllegalArgumentException();
        }
        //do a lot of things
        type3 res = //do something

        assert method1_post(old, param1, param2, res);
        assert invariant();
        return res;
    }

    protected boolean invariant(){
        // states something about myClass and return a boolean
        // OR
        // uses some assertions on some helping methods
    }

    protected boolean method1_post(myClass old, type1 param1, type3 param2, type3 res){
        // states something about res and about the modifications made on old
        // OR
        // uses some assertions on some helping methods
    }
}

这种方法的局限性：
- 没有先决条件。
- 合同不是继承的（但请注意，不变量和后置条件受到保护，可以被子类重用）。
- 没有检查不变量和后置条件不会修改我们对象的状态，因此存在副作用的风险。
- 合同并没有明确地包含在我们的文档中。
- 我们需要让每个类都可以克隆。

现在，一些问题：
- 这种方法对表演有任何影响吗？我的意思是如果禁用断言，JIT 编译器甚至会删除 old 和 res 局部变量？
- 你觉得这种方法有什么缺点吗？为什么不在课堂上使用它？
- 你能提出任何改进的建议吗？

感谢您的阅读和您的意见。

Answer 1

这并不可怕，事实上它是在你之前被别人写过的。例如，请参阅 Liskov/Guttag 的 Program Development in Java，它采用您的方法进行不变量检查，但将其称为 repOK() 而不是 invariant()。

在有限的应用程序中，它有点工作。但是，合约规范不必担心真正的代码会遇到的那种“谁在打电话给谁”的问题，这会带来很多问题。

• 假设您有一些方法 F，它调用另一个方法 G。想象一下，F 在运行时破坏了代表不变量，但在返回之前修复了问题。这是允许的，在某些情况下是必需的，但 G 不知道这一点，它会错误地引发异常。
• 构造函数更糟糕。假设 D 类扩展了 C 类并覆盖了 invariant()。 D() 调用 C()，后者调用 D.invariant()，这是错误的。 C 不必满足 D 的不变量，它比它自己的要强。
• 如果类外部的客户端向方法传递了错误的参数，则 IllegalArgumentException 是可以的。但是如果调用者在类内，这是一个常规的旧合同违反。你想区分这两者。如果您有兴趣，Gary Leavens 将在此 paper 中讨论 JML 是如何做到的。
• 以其他类方法表示的后置条件（即“后置条件”）在检查时会导致无限相互递归。

我的看法是 DbC 很有趣，如果该语言有它（或者更好的是，像 Python 的函数装饰器之类的东西），或者你有像 Modern Jass 这样的工具，然后深入研究。但是用纯 Java 做不可行。也就是说，我正在研究一个不变量检查tool，它生成的代码类似于你在这里的代码，减去调用链问题（它通过扩展类来接受一个知道什么时候做的访问者来工作查看）。需要Eclipse，有自己的问题（主要是private、static等不好的词），但是检查机制是纯Java的。

Answer 2

如果您想要 Java 的“契约式设计”，您可能想看看（真正的）大人物是如何做到的！以下是 Google 最近对“Java 合同”主题的看法：

http://google-opensource.blogspot.com/2011/02/contracts-for-java.html

现在回答你的两个问题：

- do you see any downside of this approach? Why wouldn't you use this in your classes?

因为一个缺点是它非常冗长：冗长到使代码几乎不可读。

- can you suggest any improvement?

不要重新发明轮子...

Answer 3

你觉得这有什么缺点吗 方法？你为什么不使用这个 你的课？

我编写的大多数 Java 类都不可克隆，因为在 Java 中实现 Clonable 并不容易。因此，当不是绝对必要时，我不会实施它。我不想仅仅为了你的方法而这样做。