Передумо́ва — в програмуванні та формальних методах, передумовою виконання функції є правило, яке визначає, за яких умов функція матиме визначену поведінку. Передумова є частиною формальної специфікації і використовується для верифікації програм: в разі виконання передумов, мусять, відповідно, виконуватись і всі післяумови, в іншому випадку, функція не коректна.
Концепція перед- та після умов використовується в формальній семантиці для створення основ для аксиоматичної семантики. Кінцевою метою є доведення правильності програми, виходячи із доведення правильності кожної окремої функції відповідно до її перед- та після- умов.
Інструментальна підтримка ред.
Часто, передумови просто описуються в коментарях до задіяної частини коду. Іноді, передумови перевіряються в тексті програми із допомогою тверджень. Деякі із мов програмування підтримують можливість визначення передумов безпосередньо у вихідному тексті програм. Наприклад, функція обчислення факторіалу на мові програмування Eiffel матиме такий вигляд:
factorial(n: INTEGER): INTEGER -- Обчислення факторіалу цілого числа. Число має бути додатнім. require not_negative: n >= 0 do if n = 0 then Result := 1 else Result := n * factorial(n - 1) end end
Джерела інформації ред.
- Vorbedingung (Informatik) — стаття в німецькомовній вікіпедії.
- Precondition — стаття в англомовній вікіпедії.
- Precondición (текст прикладу) — стаття в іспаномовній вікіпедії.