如何在java类方法或构造函数中插入前置条件？

Question

这是我正在参加的java课程.该书提到了先决条件和后置条件,但没有给出任何如何编码它们的例子.它继续讨论断言,我把它断了下来,但我正在做的赋值具体说明插入前置条件并用断言测试前置条件.

任何帮助都会很棒.

Answer 1

诸如Eiffel之类的语言支持“前置条件”和“后置条件”作为该语言的基本组成部分。

一个令人信服的论点是，“对象构造函数”的全部目的就是建立“类不变式”。

但是对于Java（几乎与其他所有后C ++面向对象语言一样），您几乎必须伪造它。

这是有关利用Java“断言”的出色技术说明：

• http://docs.oracle.com/javase/8/docs/technotes/guides/language/assert.html

Answer 2

这里给出的一些例子将前提条件表达为参数验证，并在断言中运用它们。非私有方法应始终执行参数验证，因为其调用者超出了其实现的范围。

我倾向于认为，在面向对象系统的上下文中，参数验证并不构成先决条件 - 尽管我在谷歌领域看到了很多这种方法的例子。

我对合约的理解是从[BINDER1999]开始的；根据被测对象的状态定义了不变式、前置条件和后置条件；表示为布尔谓词。这种处理考虑了如何管理类封装的状态空间，其中方法表示状态之间的转换。

根据参数和返回值讨论前置条件和后置条件比根据状态空间进行讨论更容易表达！所以我明白为什么这种观点更为普遍。

回顾一下，正在讨论的合同分为三种类型：

• 不变量是对被测对象的测试，从构造结束（任何构造函数）到销毁开始（尽管在转换发生时它可能会被破坏）都是如此。
• 前置条件是对被测对象的测试，必须满足该前提条件才能在被测对象上调用被测方法。
• 后置条件是对被测对象的测试，在被测方法完成后必须立即为真。

如果您采用重载方法必须在语义上等效的（明智的）方法，那么对于类中给定方法的任何重载，前置条件和后置条件都是相同的。

当考虑继承性和重写方法时，契约驱动设计必须遵循里氏替换原则；这导致以下规则：

• 派生类的不变量是其局部不变量与其基类的逻辑与。
• 重写方法的前提条件是其本地前提条件与其基类中的方法的逻辑或。
• 重写方法的后置条件是其本地后置条件与其基类中的方法的逻辑与。

当然，请记住，每当测试前置条件或后置条件时，也必须测试被测类的不变量。

在 Java 中，契约可以写成受保护的布尔谓词。例如：

    // class invariant predicate
    protected bool _invariant_ ()
    {
        bool result = super._invariant_ (); // if derived
        bool local  = ... // invariant condition within this implementation
        return result & local;
    }
    
    protected bool foo_pre_ ()
    {
        bool result = super.foo_pre_ (); // if foo() overridden
        bool local  = ... // pre-condition for foo() within this implementation
        return result || local;
    }
    
    protected bool foo_post_ ()
    {
        bool result = super.foo_post_ (); // if foo() is overridden
        bool local  = ... // post-condition for foo() with this implementation
        return result && local;
    }
    
    public Result foo (Parameters... p)
    {
        boolean success = false;
        assert (_invariant_ () && foo_pre_ ()); // pre-condition check under assertion
        try
        {
            Result result = foo_impl_ (p); // optionally wrap a private implementation function
            success = true;
            return result;
        }
        finally
        {
            // post-condition check on success, or pre-condition on exception
            assert (_invariant_ () && (success ? foo_post_ () : foo_pre_ ());
        }
    }
    
    private Result foo_impl_ (Parameters... p)
    {
        ... // parameter validation as part of normal code
    }

不要将不变量谓词滚动到前置条件或后置条件谓词中，因为这会导致在派生类中的每个测试点多次调用不变量。

这种方法对被测方法使用包装器，其实现现在位于私有实现方法中，并且实现的主体不受合约断言的影响。包装器还处理异常行为 - 在这种情况下，如果实现抛出异常，则会再次检查前置条件，正如异常安全实现所期望的那样。

请注意，在上面的示例中，如果 'foo_impl_()' 抛出异常，并且 'finally' 块中的后续前置条件断言也失败，那么来自 'foo_impl_()' 的原始异常将丢失，而有利于断言失败。

请注意，以上内容是我凭空想象的，因此可能包含错误。

参考：

• [BINDER1999] Binder，“测试面向对象的系统”，Addison-Wesley 1999。

更新2014-05-19

我回到了关于投入和产出合同的基础上。

上面的讨论基于 [BINDER1999]，从被测对象的状态空间角度考虑了契约。将类建模为强封装的状态空间是以可扩展的方式构建软件的基础 - 但这是另一个主题......

考虑在考虑继承时如何应用（和要求）里氏替换原则 (LSP) 1 ：

派生类中的重写方法必须可以替换基类中的相同方法。

为了可替换，派生类中的方法对其输入参数的限制不得比基类中的方法更严格 - 否则它将在基类方法成功的地方失败，从而破坏 LSP 1。

类似地，输出值和返回类型（不是方法签名的一部分）必须可以替换基类中方法生成的值 - 它必须至少对其输出值具有同样的限制，否则这也会破坏 LSP 1 . 请注意，这也适用于返回类型 - 可以从中导出协变返回类型的规则。

因此，重写方法的输入和输出值的契约分别在继承以及前置条件和后置条件下遵循相同的组合规则；为了有效地实施这些规则，它们必须与其适用的方法分开实施：

    protected bool foo_input_ (Parameters... p)
    {
        bool result = super.foo_input_ (p); // if foo() overridden
        bool local  = ... // input-condition for foo() within this implementation
        return result || local;
    }
    
    protected bool foo_output_ (Return r, Parameters... p)
    {
        bool result = super.foo_output_ (r, p); // if foo() is overridden
        bool local  = ... // output-condition for foo() with this implementation
        return result && local;
    }

请注意，它们几乎分别与foo_pre_()和foo_post_()相同，并且应该在测试工具中与这些合约相同的测试点处调用。

前置条件和后置条件是为方法系列定义的 - 相同的条件适用于方法的所有重载变体。输入和输出契约适用于特定的方法签名；然而，为了安全且可预测地使用这些，我们必须了解我们的语言和实现的签名查找规则（参见C++ using）。

请注意，在上面，我使用表达式Parameters... p作为任何参数类型和名称集的简写；它并不意味着暗示可变参数方法！