Пошук та усунення помилок

Едсгер Дейкстра, зробивши свій внесок до перегляду принципів складання програм і створення самих мов програмування, на цьому не заспокоївся. Не менше, ніж оператор GOTO, його дратували відлагодження та тестування – складові завершального етапу створення будь-якого програмного забезпечення. На тестування та відлагодження часто потрібно більше часу, ніж на інші фази розробки програми, разом узяті. До того ж, як вказував Дейкстра, тестування може показати лише наявність помилок, але не їх відсутність. Навіть коли здавалося, що програма повністю відлагоджена, нові вхідні дані могли викликати відмову, або, як говорять програмісти, “аварію”.

Замість того, щоб займатися тестуванням програм, Дейкстра запропонував перевіряти їх математичними методами. Стосовно маленьких програм йому вдалося добитися певних успіхів, проте великі програми не піддавалися таким прийомам. Дейкстра визнав, що це завдання важко досяжне, але не обов’язково нереальне.

Останнім часом широко звстосовується технологія попереднього моделювання та верифікації і розробки програм за допомогою скінченних автоматів – MODEL CHECKING. При цьому кожна верхівка таких автоматів передбачає опис дій, які мають виконуватись у відповідному стані автомату. Вони описуються спеціальним чином за допомогою так званих структур Крипке із застосуванням темпоральної логіки. Остання визначає порядок виконання певних дій і забезпечує синхронізацію виконання окремих гілок (потоків) програм у часі. Ця технологія широко застосовується для створення розподілених та паралельних програм і на даний час має реальне промислове впровадження. Автори цієї технології – Е. Кларк, О. Грамберг та Д. Пелед нагароджені престижною премією імені А. Тюринга в галузі комп'ютерних наук.