何时添加前置条件以及何时（仅）抛出异常？
我正在学习先决条件以及何时使用它们。有人告诉我 前提条件
@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 声明（如果 避免它们就是这里所做的）？
I am learning about preconditions and when to use them. I have been told
that the precondition
@pre fileName must be the name of a valid file
does not suit in the following code:
/**
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
Why is this?
Edit: Another example
We are assuming that the following, as an example, is done the "right" way.
Note the IllegalArgumentException and the precondition. Note how the behavior
is well defined, and how the throws declaration is made even though
a precondition is set. Most importantly, notice how it doesn't contain
a precondition for the NullPointerException. Once again, why doesn't it?
/**
* @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
Are these examples avoiding use of extra preconditions? One could
argue that if we are avoiding preconditions, then why have them at all?
That is, why not replace all preconditions with @throws declarations (if
avoiding them is what is done here)?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
维基百科将前提条件定义为：
在您的示例中，定义了文件名无效时该方法的效果（它必须抛出
FileNotFoundException）。换句话说，如果
file有效是一个先决条件，我们就知道它始终有效，并且合约中强制抛出异常的部分永远不会适用。无法到达的规范情况是一种代码味道，就像无法到达的代码一样。编辑：
当然，但是这不再是霍尔定义的先决条件。正式来说，一个方法具有前置条件
pre和后置条件post意味着该方法的每次执行都以状态prestate开始并以状态结束poststate如果蕴含的左侧为 false，则无论
poststate是什么，这都是简单的 true，即该方法将满足其契约，无论它做什么，即该方法的行为未定义。现在，快进到现代，方法可以抛出异常。对异常建模的通常方法是将它们视为特殊的返回值，即异常是否发生是后置条件的一部分。
如果 throws 子句是后置条件的一部分，那么您会得到类似这样的内容：
这在逻辑上相当于
，即，您是否编写那个 throws 子句并不重要，这就是为什么我称该规范情况不可访问。
不; throws 条款是合同的一部分，因此如果合同被破坏，则没有任何影响力。
当然，可以定义无论前提条件如何都需要满足@throws子句，但这有用吗？考虑一下：
如果
foo为null是否必须抛出异常？在经典定义中，它是未定义的，因为我们假设没有人会为foo传递null。在您的定义中，我们必须在每个 throws 子句中明确重复这一点：如果我知道没有合理的程序员会将
null传递给该方法，为什么我应该被迫在规范中指定这种情况？描述对调用者无用的行为有什么好处？ （如果调用者想知道 foo 是否为 null，他可以自己检查，而不是调用我们的方法并捕获 NullPointerException！）。Wikipedia defines precondition as:
In your example, the effect of the method if the filename is invalid is defined (it must throw a
FileNotFoundException).Put differently, if
filebeing valid were a precondition we'd know that it was always valid, and the part of the contract that mandates an exception is thrown it is wasn't would never apply. Unreachable specification cases are a code smell just like unreachable code.Edit:
Of course, but then it's no longer a precondition as defined by Hoare. Formally speaking, that a method has precondition
preand postconditionpostmeans that for each execution of the method that started in stateprestateand ended in statepoststateIf the left hand side of the implication is false, this is trivially true irrespective of what
poststateis, i.e. the method will satisfy its contract irrespective of what it does, i.e. the method's behaviour is undefined.Now, fast forward to modern times, where methods can throw exceptions. The usual way to model exceptions is to treat them as special return values, i.e. whether an exception occurred is part of the postcondition.
If the throws clause is part of the postcondtion, you have something like:
which is logically equivalent to
that is, it doesn't matter whether you write that throws clause, which is why I called that specification case unreachable.
No; the throws clause is part of the contract, and as such carries no weight if the contract is broken.
Of course it is possible to define that @throws clauses need to be satisfied irrespective of the precondition, but is that useful? Consider:
Must the exception be thrown if
fooisnull? In the classic definition, it is undefined, because we assume nobody will passnullforfoo. In your definition, we have to explicitly repeat that in every throws clause:If I know no reasonable programmer is going to pass
nullto that method, why should I be forced to specify that case in my specification? What benefit does it have to describe behavior that is not useful to the caller? (If the caller wants to know whether foo is null, he can check it himself rather than calling our method and catching the NullPointerException!).好的，这就是我发现的：
背景
基于以下原则，如 Bertrand Meyer 的书中所述
面向对象的软件构建：
，这两点回答了这个问题：
系统。尽管如此，在调试系统时会打开断言来执行此测试。
有关何时、为何以及如何使用先决条件的更多信息：
因此，只有在确定客户承担责任时，才应存在先决条件。
由于服务器不应该不测试前提条件，因此行为变得不确定（正如维基百科上所述）。
答案
第一个
@throws声明暗示该方法具有（除了断言之外）测试了前提条件。这就违反了第二点。
至于空指针；这表明空指针责任已分配
到服务器。即用“宽容的态度”，而不是“苛求的态度”。
这完全没问题。如果一个人选择采取一种苛求的态度，那么他就会
删除 throws 声明（但更重要的是；不对其进行测试），并添加
前提条件声明（也许还有断言）。
Ok, so this is what I've found out:
Background
Based on the following principles, as described in Bertrand Meyer's book
Object Oriented Software Construction:
, these two points answer this question:
system. Although, assertions are turned on to do this testing when debugging the system.
More on when, why, and how to use preconditions:
So a precondition should only exist if it is decided that the client holds the responsibility.
Since the server should not test the precondition, the behaviour becomes undefined (as also stated on Wikipedia).
Answers
the first
@throwsdeclaration implies that the method has (other than an assertion)tested the precondition. This violates the second point.
As for the null pointer; this shows that the null pointer responsibility is assigned
to the server. That is, using a "tolerant attitude", as opposed to a "demanding attitude".
This is perfectly OK. If one chose to implement a demanding attitude, one would
remove the throws declaration (but more importantly; not test for it), and add
a precondition declaration (and perhaps an assertion).
我认为按契约思想设计（我自己还没有使用它）和前置/后置条件旨在保证从该方法传入和传出的特定条件。特别是编译器（在这种情况下，理论上因为 Java 没有内置的）需要能够验证合同条件。在您的文件前提条件的情况下，这是无法完成的，因为文件是外部资源，类可能会移动并且相同的文件可能不存在等等。编译器（或预处理器）如何保证这样的合同？
另一方面，如果您只是使用它进行注释，那么它至少会向其他开发人员显示您所期望的内容，但您仍然必须预料到当文件不退出时会出现异常。
我认为它“不适合”合同设计正式意义上的方法，因为它甚至无法针对一种情况进行验证。也就是说，您可以在一种环境中给出有效的文件名，但在程序外部的其他环境中可能无效。
另一方面，日期示例、前置条件和后置条件可以在调用者上下文中进行验证，因为它们不受方法本身无法控制的外部环境设置的影响。
I think that design by contract idea (I don't use it myself yet) and pre/post conditions are intended to guarantee specific conditions incoming and outgoing from the method. Particularly the compiler (in this case, theoretically as Java does not have this built-in) would need to be able to validate the contract conditions. In the case of your file precondition, this cannot be done since the file is an external resource, the class may move and the same file may not be there, etc. How can a compiler (or pre-processor) guarantee such a contract?
On the other hand, if you are just using it for comments then it would at least show the other developer what you expect but you must still expect too that there will be exceptions when the file does not exit.
I think that it "does not suit" the method in the formal sense of design by contract because it cannot be validated for even one case. That is, you may give valid file names in one environment but that may not be valid in other environment external to your program.
On the other hand, the date example, the pre and post conditions can be validated in the caller context as they are not influenced by external environmental setup that the method itself has no control over.