Википедия определяет предусловие как:
В компьютерном программировании предварительным условием является условие или предикат, которые всегда должны быть истинными непосредственно перед выполнением некоторого раздела кода или перед операцией в формальной спецификации.
Если предварительное условие нарушается, действие раздела кода становится неопределенным и, следовательно, может выполнять или не выполнять запланированную работу.
В вашем примере, эффект метода, если имя файла неверно , определено (оно должно выдать FileNotFoundException).
Другими словами, если бы file, являющийся действительным, был предварительным условием, мы бы знали, что оно всегда было действительным, и та часть контракта, которая предписывает исключение, выбрасывается, но это не будет применяться никогда. Недостижимые случаи спецификации являются запахом кода, как и недоступный код.
Редактировать
Если у меня есть некоторые предварительные условия и я могу обеспечить определенное поведение для этих условий, разве не лучше, если я это сделаю?
Конечно, но тогда это больше не является предварительным условием, определенным Хоаром. Формально говоря, что метод имеет предусловие 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 должны выполняться независимо от предварительного условия, но полезно ли это? Рассмотрим:
@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!).