Інваріант (програмування)

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

В програмуванні, інваріант — це умова, що не змінюється, або не повинна змінюватись коли система працює правильно.

Інваріантом називають логічний вираз, що є істинним після кожного проходу тіла циклу (після виконання фіксованого оператора) і перед початком виконання циклу, який залежить від змінних, які в свою чергу змінюються в тілі циклу. Інваріанти використовуються в теорії верифікації програм для доказу правильності виконання циклу. Також інваріанти використовують при проектуванні циклічних алгоритмів.

Як приклад, можна навести код комп'ютерної програми що повторно обробляє деякі дані. Часто трапляється так, що деякі дані можуть змінюватись, а деякі повинні не змінюватись.

У комп'ютерних науках, такі технології як оптимізуюча компіляція, розробка за контрактом та формальні методи приділяють багато уваги до інваріантів у програмах.

Див. також

[ред. | ред. код]

Посилання

[ред. | ред. код]