4

我正在学习先决条件以及何时使用它们。我被告知前提条件

@pre fileName must be the name of a valid file

不适合以下代码：

/**
Creates a new FileReader, given the name of file to read from.
@param fileName- the name of file to read from
@throw FileNotFoundException - if the named file does not exist,
is a directory rather than a regular file, or for some other reason cannot
be opened for reading.
*/
public FileReader readFile(String fileName) throws FileNotFoundException {
. . .
}//readFile

为什么是这样？

编辑：另一个例子

作为示例，我们假设以下内容是以“正确”的方式完成的。请注意 IllegalArgumentException 和前提条件。请注意行为是如何定义良好的，以及即使设置了前提条件也是如何进行 throws 声明的。最重要的是，请注意它不包含 NullPointerException 的先决条件。再说一遍，为什么不呢？

/**
* @param start the beginning of the period
* @param end the end of the period; must not precede start
* @pre start <= end
* @post The time span of the returned period is positive.
* @throws IllegalArgumentException if start is after end
* @throws NullPointerException if start or end is null
*/
public Period(Date start, Date end) f

这些示例是否避免使用额外的先决条件？有人可能会争辩说，如果我们要避免先决条件，那为什么还要有它们呢？也就是说，为什么不用@throws 声明替换所有前提条件（如果避免它们是这里所做的）？

4

3 回答 3

4

维基百科将前提条件定义为：

在计算机编程中，前置条件是一个条件或谓词，在执行某些代码部分之前或在正式规范中的操作之前必须始终为真。

如果违反了先决条件，则代码部分的效果将变得未定义，因此可能会或可能不会执行其预期工作。

在您的示例中，如果文件名无效，则方法的效果已定义（它必须抛出一个FileNotFoundException）。

换句话说，如果file有效是一个先决条件，我们就会知道它总是有效的，并且合约中要求异常的部分被抛出，它不是永远不会适用。无法访问的规范案例是一种代码味道，就像无法访问的代码一样。

编辑：

如果我有一些先决条件，并且可以为这些条件提供定义的行为，那么这样做不是更好吗？

当然，但它不再是 Hoare 定义的先决条件。形式上来说，一个方法有前置条件pre和后置条件post是指方法的每一次执行都以状态开始，以状态prestate结束poststate

pre(prestate) ==> post(poststate)

如果暗示的左边是假的，那么无论是什么，这都是微不足道的poststate，即该方法将满足其契约而不管它做什么，即该方法的行为是未定义的。

现在，快进到现代，方法可以抛出异常。对异常建模的常用方法是将它们视为特殊的返回值，即是否发生异常是后置条件的一部分。

不过，异常并非真的无法访问，是吗？

如果 throws 子句是 postcondtion 的一部分，你有类似的东西：

pre(prestate) ==> (pre(prestate) and return_valid) or (not pre(prestate) and throws_ exception)

这在逻辑上等价于

pre(prestate) ==> (pre(prestate) and return_valid)

也就是说，你是否写了 throws 子句并不重要，这就是为什么我称那个规范案例不可达的原因。

我想说的是，一个例外是作为先决条件的补充，以告知用户如果他/她违反合同将会发生什么。

不; throws 条款是合同的一部分，因此如果合同被破坏，则不会产生任何影响。

当然，可以定义无论前置条件如何都需要满足 @throws 子句，但这有用吗？考虑：

@pre foo != null
@throws IllegalStateException if foo.active

foo如果是，必须抛出异常null吗？在经典定义中，它是未定义的，因为我们假设没有人会通过null. foo在您的定义中，我们必须在每个 throws 子句中明确重复这一点：

@pre foo != null
@throws NullPointerException if foo == null
@throws IllegalStateException if foo != null && foo.active

如果我知道没有合理的程序员会传递null给该方法，我为什么要被迫在我的规范中指定这种情况？描述对调用者无用的行为有什么好处？（如果调用者想知道 foo 是否为 null，他可以自己检查，而不是调用我们的方法并捕获 NullPointerException！）。

于 2011-04-19T19:42:19.657 回答
3

好的，这就是我发现的：

背景

基于以下原则，如 Bertrand Meyer 的著作 Object Oriented Software Construction中所述：

“非冗余原则在任何情况下，例程的主体都不应测试例程的前提条件。” ——伯特兰·迈耶

“前提条件可用性规则 出现在例程的前提条件中的每个功能都必须可供该例程可用的每个客户端使用。” ——伯特兰·迈耶

，这两点回答了这个问题：

  1. 为了使前提条件有用，客户（方法的用户）必须能够测试它们。
  2. 服务器永远不应该测试前提条件，因为这会增加系统的复杂性。虽然，在调试系统时会打开断言来执行此测试。

更多关于何时、为什么以及如何使用前置条件：

“按合同设计的核心理念是，以非冗余原则表示，对于任何可能危及例程正常运行的一致性条件，您应该仅将该条件的执行分配给合同中的两个合作伙伴之一。哪一个? 在每种情况下，您有两种可能性： • 将责任分配给客户，在这种情况下，条件将作为例行程序前提条件的一部分出现。 • 或者您指定供应商，在这种情况下，条件将出现在有条件的指令中例程主体中的 if condition then ... 或等效控制结构的形式。

我们可以称第一种态度是苛刻的，而第二种态度是宽容的。”——伯特兰·迈耶

因此，只有在确定客户承担责任时，才应存在先决条件。由于服务器不应测试先决条件，因此行为变得未定义（也如 Wikipedia 所述）。

答案

  • 第一点回答了第一个例子。
  • 至于第二个例子，它可能没有以正确的方式完成。这是因为第一个@throws声明意味着该方法已经（不是断言）测试了前提条件。这违反了第二点。

至于空指针；这表明空指针责任已分配给服务器。也就是说，使用“宽容的态度”，而不是“要求的态度”。这完全没问题。如果选择实施一种要求的态度，则可以删除 throws 声明（但更重要的是；不对其进行测试），并添加一个前置条件声明（可能还有一个断言）。

于 2011-04-20T19:39:36.677 回答
2

我认为按合同设计的理念（我自己还没有使用它）和前置/后置条件旨在保证从方法传入和传出的特定条件。特别是编译器（在这种情况下，理论上因为 Java 没有这个内置）需要能够验证合同条件。在您的文件前置条件的情况下，这是无法做到的，因为文件是外部资源，类可能会移动并且相同的文件可能不存在等等。编译器（或预处理器）如何保证这样的合同？

另一方面，如果您只是将它用于评论，那么它至少会向其他开发人员展示您的期望，但您仍然必须期望当文件不退出时会有异常。

我认为它“不适合”合同设计形式意义上的方法，因为它甚至无法验证一个案例。也就是说，您可以在一个环境中提供有效的文件名，但在程序外部的其他环境中可能无效。

另一方面，日期示例、前置条件和后置条件可以在调用者上下文中验证，因为它们不受方法本身无法控制的外部环境设置的影响。

于 2011-04-19T21:49:16.183 回答