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

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

Післяумови, відіграють, також, важливу роль і в менш формальному тестуванні, оскільки легко можна порівняти результати тестів із післяумовами. Такий підхід використовується в так званих модульних тестах.

Приклади написання

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

$max(i:𝐙,j:𝐙)r:𝐙$

$\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$

$\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t}(r=i\vee r=j)\wedge i\le r\wedge j\le r$

Джерела інформації

• Nachbedingung (Informatik) — стаття в німецькомовній вікіпедії.
• Cliff B Jones, «Systematic software development using VDM, second edition», The University, Manchester, England.

Див. також

• Передумова (формальні методи)
• Твердження (програмування)