Page 56 - 4592

 Формальний підхід або доказ застосовується, коли з

вихідних формул-аксіом за допомогою формальних
процедур (правил виводу) виводяться шукані формули і
затвердження (теореми). Висновок здійснюється шляхом
переходу від одних формул до інших за суворими

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

що з його допомогою вдається уникати звернень до
нескінченної області значень і на кожному кроці докази
оперувати тільки кінцевим безліччю символів.

 Інтерпретаційний підхід застосовується, коли здійснюється
підстановка констант у формули, а потім інтерпретація
формул, як осмислених тверджень в елементах множин

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

вичерпної перевірки можуть виявитися досить великі.
Інтерпретаційний підхід використовується при
експериментальній перевірці відповідності програми своєї

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

Налагодження (debug, debugging) - процес пошуку,
локалізації та виправлення помилок в програмі.
Термін «налагодження» у вітчизняній літературі

використовується подвійно: для позначення активності з пошуку
помилок (власне тестування), по знаходженню причин їх появи та
виправлення, або активності по локалізації та виправлення

помилок.
Тестування - це процес виконання ПО системи або
компонента в умовах аналізу або запису одержуваних результатів

з метою перевірки (оцінки) деяких властивостей тестованого
об'єкта.

56