ПРОГРАМА складної структури з використанням меню

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

Четвертою формою статичного контролю програм є їх верифікація, тобто аналітичний доказ їх коректності.

У інтуїтивному значенні під коректністю розуміють властивості програми, що свідчать про відсутність в ній помилок, допущених розробником на різних етапах проектування ( специфікації, проектування алгоритму і структур даних, кодування ). Коректність самої програми по відношенню до цілей, поставлених перед її розробкою ( тобто ця відносна властивість ). Відмінність поняття коректності і надійності програм в наступному:

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

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

Надійність можна представити сукупністю наступних характеристик:

1) цілісність програмного засобу (здатність його до захисту від відмов);

2) живучість (здібність до вхідного контролю даних і їх перевірки в ході роботи);

3) завершеність (бездефектність готового програмного засобу, характеристика якості його тестування);

4) працездатність (здатність програмного засобу до відновлення своїх можливостей поле збоїв).

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

5

З урахуванням специфіки появи помилок в програмах можна виділити дві сторони поняття коректності:

1) коректність як точна відповідність цілям розробки програми (які відображені в специфікації) при умові її завершення або часткова коректність;

2) завершення програми, тобто досягнення програмою в процесі її виконання своєї кінцевої точки.

У залежності від виконання або невиконання кожного з двох названих властивостей програми розрізнюють шість задач аналізу коректності:

1) доказ часткової коректності;

2) доказ часткової некоректність;

3) доказ завершення програми;

4) доказ незавершення програми;

5) доказ тотальної (повної ) коректності (тобто одночасне рішення першої і третьої задач);

6) доказ некоректність (рішення другої або четвертої задачі).