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

How do I insert a precondition in a java class method or constructor?

提问by Jay Rohrssen

This is for a java class I'm taking. The book mentions preconditions and postconditions but doesn't give any examples how to code them. It goes on to talk about asserts, I have that down, but the assignment I'm doing specifically states to insert preconditions and test the preconditions with asserts.

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

Any help would be great.

任何帮助都会很棒。

回答by paulsm4

Languages like Eiffel support "preconditions" and "postconditions" as a basic part of the language.

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

One can make a compelling argument that the whole purpose of an "object constructor" is preciselyto establish "the class invariant".

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

But with Java (as with just about every other post-C++ object oriented language), you pretty much have to fake it.

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

Here's an excellent tech note on leveraging Java "assert":

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

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

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

回答by simon.watts

Some examples given here express preconditions as parameter validation, and exercise them in assertions. A non-private method should always perform parameter validation as its caller is out of scope of its implementation.

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

I tend to argue that parameter valdiation does not constitute a precondition, in the context of object oriented systems - although I see plenty of examples of this approach in the google-sphere.

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

My understanding of contracts started with [BINDER1999]; which defined invariant, precondition, and postconditions in terms of the state of the object-under-test; expressed as Boolean predicates. This treatment considers how the state-space encapsulated by a class is managed, in which methods represent transitions between states.

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

Discussion of pre- and post-conditions in terms of parameter and return values is much easier to convey than discussions in terms of state-spaces! So I can see why this view is much more prevalent.

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

To recap, there are three types of contract under discussion:

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

• The invariantis a test on the object-under-test which is true from the end of construction (any constructor), to the start of its destruction (although it may be broken while a transition is taking place).
• A pre-conditionis a test on the object-under-test which must be true for the method-under-test to be invoked on the object-under-test.
• A post-conditionis a test on the object-under-test which must be true immediately after the method-under-test completes.

• 该不变的是物体被测这从施工（任何构造）的端部如此，它的破坏的开始（尽管它可以同时过渡正在发生断裂）上的测试。
• 甲先决条件是物体被测了必须为方法被测是真实的在测试待测对象上被调用。
• 甲后置条件是在物体被测方法被测完成后立即必须是真实的测试。

If you adopt the (sensible) approach that overloaded methods must be semantically equivalent, then pre- and post-conditions are the same for any overload of a given method in a class.

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

When interitance and overridden methods are considered, contract-driven-design must follow the Liskov Substitution Principle; which results in the following rules:

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

• The invariantof a derived class is the logical-AND of its local invariant, and that of its base class.
• The pre-conditionof an overridden method is the logical-OR of its local pre-condition, and that of the method in its base class.
• The post-conditionof an overridden method is the logical-AND of its local post-condition, and that of the method in its base class.

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

Remember, of course, that whenever a pre- or post-condition is tested, the invariant for the class-under-test must also be tested.

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

In Java, contracts can be written as protected Boolean predicates. For example:

在 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
}

Don't roll the invariant predicate into the pre- or post-condition predicates, as this would result in the invariant being called multiple times at each test-point in a derived class.

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

This approach uses a wrapper for the method-under-test, the implementation for which is now in a private implementation method, and leaves the body of the implementation unaffected by the contract assertions. The wrapper also handles exceptional behaviour - in this case, if the implementation throws and exception, the pre-condition is checked again, as expected for an exception-safe implementation.

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

Note that if, in the example above, 'foo_impl_()' throws an exception, and the subsequent pre-condition assertion in the 'finally' block also fails, then the original exception from 'foo_impl_()' will be lost in favour of the assertion failure.

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

Please note that the above is written off the top-of-my-head, so may contain errors.

请注意，以上内容是我的头顶上写的，因此可能包含错误。

Reference:

参考：

• [BINDER1999] Binder, "Testing Object-Oriented Systems", Addison-Wesley 1999.

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

---

---

Update 2014-05-19

更新 2014-05-19

I have gone back-to-basics with regards to contracts on input and outputs.

关于输入和输出的合同，我已经回到了基础。

The discussion above, and based on [BINDER1999], considered contracts in terms of the state-space of objects-under-test. Modelling classes as strongly encapsulated state-spaces is fundamental to building software in a scalable manner - but that is another topic...

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

Considering how the Lyskov Substitution Principle (LSP) 1is applied (and required) when considering inheritance:

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

An overridden method in a derived class must be substitutable for the same method in the base class.

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

To be substitutable, the method in the derived class must not be more restrictive on its input parameters than the method in the base class - otherwise then it would fail where the base class method succeeded, breaking LSP 1.

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

Similarly the output value(s) and return type (where not part of the method signature) must be substitutable for that produced by the method in the base class - it must be at least as restrictive in its output values otherwise this also would break LSP 1. Note that this also applies to the return type - from which rules on co-variant return types can be derived.

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

Therefore contracts on the input and output values of an overridden method follow the same rules for combination under inheritance and pre- and post-conditions respectively; and in order to implement these rules effectively they must be implemented separate from the method to which they apply:

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

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;
}

Note that these are almost identical to foo_pre_()and foo_post_()respectively, and should be called in the test harness at the same test-points as these contracts.

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

The pre- and post-conditions are defined for a method-family - the same conditions apply to all overloaded variants of a method. The input and output contracts apply to a specific method signature; however, to use these safely and predictably, we must understand the signature-lookup rules for our language and implementation (cf.C++ using).

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

Note that in the above, I use the expression Parameters... pas short-hand for any set of parameter types and names; it is notment to imply a varatic method!

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

回答by Eamonn O'Brien-Strain

Just use assertto code the preconditions. For example:

仅用于assert对前提条件进行编码。例如：

...
private double n = 0;
private double sum = 0;
...
public double mean(){
  assert n > 0;
  return sum/n;
}
...

回答by Zaheer Ahmed

A precondition is a condition that has to hold at given point in the execution of a program, if the execution of the program is to continue correctly. For example, the statement "x = A[i];" has two preconditions: that A is not null and that 0 <= i < A.length. If either of these preconditions is violated, then the execution of the statement will generate an error.

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

Also, a precondition of a subroutine is a condition that has to be true when the subroutine is called in order for the subroutine to work correctly.

此外，子例程的前提条件是在调用子例程时必须为真的条件，以便子例程正常工作。

Here is Detail&

这是详细信息&

Here is example: preconditions-postconditions-invariants

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

回答by tokhi

To apply preconditions and postconditions technique in Java you need to define and execute assertions at runtime. It actually allows to define runtime checks inside your code.

要在 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;
}

Please follow details of the above code here

请在此处按照上述代码的详细信息进行操作