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

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

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

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

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

${\displaystyle max(i:\mathbf {Z} ,j:\mathbf {Z} )r:\mathbf {Z} }$

${\displaystyle \mathrm {pre} \,\mathrm {true} }$

${\displaystyle \mathrm {post} (r=i\lor r=j)\land i\leq r\land j\leq r}$

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

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

Див. також

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