When to add a precondition and when to (only) throw an exception?

Question

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)?

Answer 1

Wikipedia defines precondition as:

In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.

If a precondition is violated, the effect of the section of code becomes undefined and thus may or may not carry out its intended work.

In your example, the effect of the method if the filename is invalid is defined (it must throw a FileNotFoundException).

Put differently, if file being 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:

If I have some preconditions, and can provide defined behavior for these conditions, wouldn't it be better if I did so?

Of course, but then it's no longer a precondition as defined by Hoare. Formally speaking, that a method has precondition pre and postcondition post means that for each execution of the method that started in state prestate and ended in state poststate

pre(prestate) ==> post(poststate)

If the left hand side of the implication is false, this is trivially true irrespective of what poststate is, 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.

The exception is not really unreachable though, is it?

If the throws clause is part of the postcondtion, you have something like:

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

which is logically equivalent to

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

that is, it doesn't matter whether you write that throws clause, which is why I called that specification case unreachable.

I would say that an exception rather works as a supplement to the precondition to inform the user of what's going to happen if he/she breaks the contract.

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:

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

Must the exception be thrown if foo is null? In the classic definition, it is undefined, because we assume nobody will pass null for foo. In your definition, we have to explicitly repeat that in every throws clause:

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

If I know no reasonable programmer is going to pass null to 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!).