В компьютерном программировании предусловие — это условие или предикат , который всегда должен быть истинным непосредственно перед выполнением некоторого раздела кода или перед операцией в формальной спецификации .
Если предусловие нарушено, эффект раздела кода становится неопределенным и, таким образом, может или не может выполнить свою предполагаемую работу. Предусловия, которые отсутствуют, недостаточны или формально не доказаны (или имеют некорректную попытку доказательства), или не проверены статически или динамически, могут привести к проблемам безопасности , особенно в небезопасных языках, которые не являются строго типизированными.
Часто предварительные условия просто включаются в документацию затронутого раздела кода. Предварительные условия иногда проверяются с использованием защит или утверждений внутри самого кода, и в некоторых языках для этого есть специальные синтаксические конструкции.
Функция факториала определена только там, где ее параметр — целое число, большее или равное нулю. Таким образом, реализация функции факториала будет иметь предварительное условие, что ее параметр будет целым числом и что параметр будет больше или равен нулю. В качестве альтернативы можно использовать систему типов языка для указания того, что параметр функции факториала — это натуральное число (целое число без знака), что может быть формально проверено автоматически проверкой типов компилятора.
Кроме того, когда числовые типы имеют ограниченный диапазон (как в большинстве языков программирования), предварительное условие должно также указывать максимальное значение, которое может иметь параметр, если переполнение не должно произойти. (например, если реализация factorial возвращает результат в виде 64-битного целого числа без знака, то параметр должен быть меньше 21, поскольку factorial(21) больше максимального целого числа без знака, которое может быть сохранено в 64 битах). Если язык поддерживает подтипы диапазона (например, Ada ), такие ограничения могут быть автоматически проверены системой типов. Более сложные ограничения могут быть формально проверены интерактивно с помощью proof assistant .
Предварительные условия в объектно-ориентированной разработке программного обеспечения являются неотъемлемой частью проектирования по контракту . Проектирование по контракту также включает понятия постусловия и инварианта класса .
Предварительное условие для любой процедуры определяет любые ограничения на состояние объекта, которые необходимы для успешного выполнения. С точки зрения разработчика программы, это составляет часть контракта вызывающего процедуру. Затем вызывающий обязан гарантировать, что предварительное условие выполняется до вызова процедуры. Вознаграждение за усилия вызывающего выражается в постусловии вызываемой процедуры . [1]
Процедура в следующем примере, написанная на Eiffel, принимает в качестве аргумента целое число, которое должно быть допустимым значением для часа дня, т. е. от 0 до 23 включительно. Предварительное условие следует за ключевым словом require. Оно указывает, что аргумент должен быть больше или равен нулю и меньше или равен 23. Тег " valid_argument:" описывает это предложение предварительного условия и служит для его идентификации в случае нарушения предварительного условия во время выполнения.
set_hour ( a_hour : INTEGER ) -- Установить `hour' в `a_hour' require valid_argument : 0 <= a_hour и a_hour <= 23 do hour := a_hour ensure hour_set : hour = a_hour end При наличии наследования процедуры, унаследованные классами-потомками (подклассами), делают это с действующими предварительными условиями. Это означает, что любые реализации или переопределения унаследованных процедур также должны быть написаны для соответствия их унаследованному контракту. Предварительные условия могут быть изменены в переопределенных процедурах, но они могут быть только ослаблены. [2] То есть переопределенная процедура может уменьшить обязательство клиента, но не увеличить его.