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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

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

Приклади написання[ред.ред. код]

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

max(i:\mathbf{Z}, j:\mathbf{Z})r : \mathbf{Z}
\mathrm{pre} \, \mathrm{true}
\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.

Див. також[ред.ред. код]