7

这是针对我正在学习的 Java 课程的。这本书提到了前置条件和后置条件，但没有给出如何编码它们的任何示例。它继续谈论断言，我把它记下来了，但是我正在做的任务专门说明插入先决条件并用断言测试先决条件。

任何帮助都会很棒。

4

5 回答 5

5

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

我倾向于争辩说，在面向对象系统的上下文中，参数验证并不构成先决条件——尽管我在 google-sphere 中看到了很多这种方法的例子。

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

在参数和返回值方面的前置条件和后置条件的讨论比在状态空间方面的讨论更容易传达！所以我明白为什么这种观点更为普遍。

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

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

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

在考虑交互和覆盖方法时，契约驱动设计必须遵循 Liskov 替换原则；这导致以下规则：

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

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

在 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]，根据被测对象的状态空间考虑了合同。将类建模为强封装的状态空间是以可扩展方式构建软件的基础 - 但这是另一个主题......

考虑在考虑继承时如何应用（和要求）Liskov 替换原则 (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作为任何一组参数类型和名称的简写；这并不意味着暗示可变参数方法！

于 2014-05-02T14:11:18.970 回答
5

像 Eiffel 这样的语言支持“前置条件”和“后置条件”作为语言的基本部分。

可以提出一个令人信服的论点，即“对象构造函数”的全部目的正是建立“类不变量”。

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

这是一篇关于利用 Java“断言”的优秀技术说明：

于 2012-11-18T18:57:14.663 回答
0

只需用于assert编码前提条件。例如：

...
private double n = 0;
private double sum = 0;
...
public double mean(){
  assert n > 0;
  return sum/n;
}
...
于 2012-11-18T19:03:23.837 回答
0

如果程序的执行要正确继续，前提条件是必须在程序执行的给定点保持的条件。例如，语句“x = A[i];” 有两个先决条件：A 不为空且 0 <= i < A.length。如果违反了这些先决条件中的任何一个，则语句的执行将产生错误。

此外，子程序的先决条件是在调用子程序时必须为真以使子程序正常工作的条件。

这是详细信息&

这是示例： 前置条件-后置条件-不变量

于 2012-11-18T19:04:46.333 回答
0

要在 Java 中应用前置条件和后置条件技术，您需要在运行时定义和执行断言。它实际上允许在代码中定义运行时检查。

public boolean isInEditMode() {
 ...
}

/**
* Sets a new text.
* Precondition: isEditMode()
* Precondition: text != null
* Postcondition: getText() == text
* @param name
*/
public void setText(String text) {
 assert isInEditMode() : "Precondition: isInEditMode()";
 assert text != null : "Precondition: text != null";

 this.text = text;

 assert getText() == text : "Postcondition: getText() == text";
}

/**
* Delivers the text.
* Precondition: isEditMode()
* Postcondition: result != null
* @return
*/
public String getText() {

 assert isInEditMode() : "Precondition: isInEditMode()";

 String result = text;

 assert result != null : "Postcondition: result != null";
 return result;
}

请在此处关注上述代码的详细信息

于 2012-11-18T19:11:17.823 回答