何时添加前置条件，何时仅抛出异常？

Question

我正在学习关于前置条件以及何时使用它们的相关知识。有人告诉我，前置条件

@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 声明替换所有的前提条件（如果在这里避免它们的话）？

- Datoraki

---

据我所知，@pre注解不是标准Java的一部分，也不是正式的“前提条件”。也许你正在使用某个库？ - leonbloy

然而，在Java中使用设计契约时，这种类型的注释并不罕见。以下是网上的一个随机示例： http://www.mmsindia.com/DBCForJava.html#Precondition - Datoraki

一些来自谷歌的随机例子：http://modernjass.sourceforge.net/http://portal.acm.org/citation.cfm?id=832856这可能是更好地解释所有意义的方法：http://www.cs.olemiss.edu/~hcc/distObj/notes/OW_Berlin99_web.pdf - Datoraki

Answer 1

维基百科对“precondition”作了如下定义：

在计算机编程中，“precondition”是指某段代码的执行或正式规范中某个操作之前必须始终为真的条件或谓词。如果违反了“precondition”，那么代码的效果就变得不可预测，可能会或可能不会执行其预期的工作。

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

换句话说，如果“file”是有效的“precondition”，我们将知道它始终有效，并且强制要求引发异常的契约部分将永远不适用。无法到达的规范情况与无法到达的代码一样令人不安。

编辑：如果我有一些前提条件，并且可以为这些条件提供明确定义的行为，那么是否最好这样做？

当然，但这就不再是Hoare所定义的“precondition”了。严格来说，方法具有“precondition pre”和“postcondition post”意味着对于每次在状态“prestate”开始并以状态“poststate”结束的方法执行。

pre(prestate) ==> post(poststate)

如果蕴含式的左侧为假，无论 poststate 是什么，这都是显然成立的，即该方法将满足其合同，无论它做什么，即该方法的行为未定义。现在，快进到现代时代，方法可以抛出异常。建模异常的通常方式是将它们视为特殊的返回值，即是否发生异常是后置条件的一部分。引用块中说：“但是异常确实是不可达的吗？”如果 throws 子句是后置条件的一部分，您会得到以下内容：

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

这在逻辑上等同于

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

也就是说，你是否写出了抛出异常的代码并不重要，这也是我称之为不可达情况的原因。

我认为，异常更像是前置条件的补充，用于告知用户如果他/她违反了合同将会发生什么。

不，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是否为空，他可以自己检查而不是调用我们的方法并捕获NullPointerException！）

- meriton

---

谢谢你的答案，但我不能同意你的看法。 听起来维基百科表示通常情况下该行为是未定义的。 我认为你有点让未定义的行为听起来像是可取的。 如果我有一些前置条件，并且可以为这些条件提供明确定义的行为， 如果我这样做不是更好吗？我的意思是说， 使得调用前置条件成为先决条件的未定义行为并没有多大意义。 - Datoraki

关于无法到达的规范情况： 但是，异常并不是真正无法到达的，对吧？ 我认为异常更像是前置条件的补充，用于告知用户如果他/她违反合同将会发生什么。你同意吗？ - Datoraki

当然，但这样就不再是Hoare定义的前提条件了。 所以：

1. 尽可能定义行为。
2. 前提条件会导致未定义的行为。

=> 最好不要使用前提条件，而只使用@throws声明。 那么，为什么还存在前提条件？您认为第二个示例应该删除@pre吗？ - Datoraki

我们必须在每个throws子句中明确重复这一点。 我不明白如何添加有关违反合同时应抛出什么异常的信息会重复自己。尽管它是合同的一部分，但它不是合同的相同部分，因为它提供了额外的信息。 “因此，如果违反合同，则没有任何作用。” 它具有权重，我可以在文档中阅读并查看如果我违反合同会得到什么异常。您认为第二个示例（如果使用@pre）是否应省略@throws？ - Datoraki

pre(prestate) ==> post(poststate) 如果蕴含式左侧为假，那么无论poststate是什么，这都是显然成立的。那么什么是显然成立的呢？如果你指整个表达式： 蕴含式总是有效的（只要变量不是t -> f），也应该如此。 如果你指右侧：如果左侧为假，则这并不影响右侧，因为这是一个蕴含而不是等价关系。 如果你指左侧：如果左侧为假，则它绝对不是真的。 你的意思非常不清楚。请重新表述一下？ - Datoraki

pre(prestate) ==> (pre(prestate) and return_valid) or (not pre(prestate) and throws_ exception) 的意思是：“如果预先状态 pre(prestate) 成立，返回有效（return_valid），否则，如果预先状态不成立，则引发异常（throws_exception）”。这里需要注意的是，pre(state) 不能保证为真，因为客户端可能会违反约定。因此，就像在 NullPointerException 上添加 @throws 以通知客户端如果发送空指针会发生什么一样，我们应该添加 @throws，对吧？即使我们没有提供有关哪些输入有效的额外信息，但是我们提供了有关方法将如何行事的额外信息（合同的一部分）。 - Datoraki

Answer 2

好的，以下是我发现的：

背景

根据Bertrand Meyer在面向对象软件构造一书中描述的以下原则：

“非冗余原则：例程体绝不应测试例程的前置条件。” - Bertrand Meyer

“前置条件可用规则：例程前置条件中出现的每个特征必须对例程可用的每个客户端都可用。” - Bertrand Meyer

这两点回答了这个问题：

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

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

“设计合同的核心思想是，根据非冗余原则，对于可能危及例程正常运行的任何一致性条件，您应该将此条件的强制执行分配给合同中的两个合作伙伴之一。哪一个？在每种情况下，您都有两种可能性：•要么将责任分配给客户端，在这种情况下，条件将出现为例程的前置条件的一部分。•或者您任命供应商，在这种情况下，条件将以if条件，然后...的形式的条件指令或等效控制结构出现在例程的主体中。

我们可以称第一个态度为要求，第二个态度为宽容。” - Bertrand Meyer

因此，只有在决定客户端承担责任时，前置条件才应存在。 由于服务器不应测试前置条件，行为变得未定义（正如维基百科上所述）。

回答

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

至于空指针；这表明空指针的责任被分配给了服务器。也就是说，使用“宽容的态度”，而不是“要求的态度”。这是完全可以的。如果选择实施要求的态度，将删除throws声明（但更重要的是；不要测试它），并添加前置条件声明（以及可能的断言）。

- Datoraki

Answer 3

我认为设计契约思想（我自己还没有使用）和前/后置条件旨在保证方法的特定条件进入和退出。特别是编译器（在这种情况下，理论上，因为Java没有内置此功能）需要能够验证合同条件。在您的文件前提条件的情况下，这是不可能的，因为文件是外部资源，类可能会移动，同一个文件可能不存在等等。编译器（或预处理器）如何保证这样的契约？

另一方面，如果您只是用它进行注释，那么至少可以向其他开发人员显示您的期望，但仍必须预期当文件不存在时会出现异常。

我认为它在设计契约的正式意义上“不适合”该方法，因为它无法验证即使一个案例。也就是说，在一个环境中你可以给出有效的文件名，但在程序外部的其他环境中可能无效。

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

- Kevin Brock

---

当然，客户端必须能够检查前提条件才能使它们有用。那么空指针呢？为什么不为其设置前提条件呢？ - Datoraki

@Datoraki，你可以设置一个前置条件来确保引用不为空。显然，如果有人仍然传递了“null”，运行时引擎仍将抛出“NullPointerException”。在一些支持设计合同的编译器/预编译器中，这将得到完全执行（例如C# 4.0），从而保证没有空引用。 - Kevin Brock