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

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

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

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

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

Див. також

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.