何时添加前置条件以及何时（仅）抛出异常？

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 声明（如果这里所做的是避免它们）？

Answer 1

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

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

如果违反前提条件，则该代码段的效果将变得不确定，因此可能会也可能不会执行其预期工作。

在您的示例中，定义了文件名无效时该方法的效果（它必须抛出 a FileNotFoundException）。

换句话说，如果file有效是一个先决条件，我们就知道它始终有效，并且合同中强制抛出异常的部分将永远不会适用。无法到达的规范情况是一种代码味道，就像无法到达的代码一样。

编辑：

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

当然，但是这不再是霍尔定义的先决条件。从形式上来说，一个方法有前置条件pre和后置条件post意味着该方法的每次执行都是以state开始prestate并以state结束的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 条款是合同的一部分，因此如果合同被破坏，则没有任何影响力。

当然，可以定义无论前提条件如何都需要满足@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！）。