Передумова (формальні методи)
Передумо́ва — в програмуванні та формальних методах, передумовою виконання функції є правило, яке визначає, за яких умов функція матиме визначену поведінку. Передумова є частиною формальної специфікації і використовується для верифікації програм: в разі виконання передумов, мусять, відповідно, виконуватись і всі післяумови, в іншому випадку, функція не коректна.
Концепція перед- та після умов використовується в формальній семантиці для створення основ для аксиоматичної семантики. Кінцевою метою є доведення правильності програми, виходячи із доведення правильності кожної окремої функції відповідно до її перед- та після- умов.
Інструментальна підтримка
Часто, передумови просто описуються в коментарях до задіяної частини коду. Іноді, передумови перевіряються в тексті програми із допомогою тверджень. Деякі із мов програмування підтримують можливість визначення передумов безпосередньо у вихідному тексті програм. Наприклад, функція обчислення факторіалу на мові програмування 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 (текст прикладу) — стаття в іспаномовній вікіпедії.