Передумова (формальні методи)

Матеріал з Вікіпедії — вільної енциклопедії.

Передумо́ва — в програмуванні та формальних методах, передумовою виконання функції є правило, яке визначає, за яких умов функція матиме визначену поведінку. Передумова є частиною формальної специфікації і використовується для верифікації програм: в разі виконання передумов, мусять, відповідно, виконуватись і всі післяумови, в іншому випадку, функція не коректна.

Концепція перед- та після умов використовується в формальній семантиці для створення основ для аксиоматичної семантики. Кінцевою метою є доведення правильності програми, виходячи із доведення правильності кожної окремої функції відповідно до її перед- та після- умов.

[ред.] Інструментальна підтримка

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