Пі́сляумова, в програмуванні та формальних методах — правило відносно результатів виконання функції, яке має виконуватись, якщо було виконано вимоги передумови. Післяумова є складовою частиною формальної специфікації функції і використовується для її верифікації: в разі виконання передумов, мусять, відповідно, виконуватись і всі післяумови, в іншому випадку, функція не коректна.
Післяумови, відіграють, також, важливу роль і в менш формальному тестуванні, оскільки легко можна порівняти результати тестів із післяумовами. Такий підхід використовується в так званих модульних тестах.
Приклади написання ред.
Зазначення післяумов підтримується в мовах формальних специфікацій. Наприклад, декларація функції находження максимального числа в парі двох цілих чисел на мові VDM матиме вигляд:
Джерела інформації ред.
- Nachbedingung (Informatik) — стаття в німецькомовній вікіпедії.
- Cliff B Jones, «Systematic software development using VDM, second edition», The University, Manchester, England.