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

Методи доказу часткової коректності програм як правило спираються на аксіоматичний підхід до формалізації семантики мов програмування. У цей час відомі аксіоматичні семантики Паськаля, підмножини ПЛ/1 і деяких інших мов.

Аксіоматична семантика мови програмування являє собою сукупність аксіом і правил висновку. За допомогою аксіом задається семантика простих операторів мови (привласнення, введення - виведення, процедур). За допомогою правил висновку описується семантика складових операторів або керуючих структур (послідовності, умовного вибору, циклів). Серед цих правил висновку треба відмітити правило висновку для операторів циклу оскільки воно вимагає знання інваріанта циклу (формули, істинності якій не змінюється при будь-якому проходженні циклу).

Побудова інваріанта для оператора циклу по його тексту є алгоритмічно не вирішуваної задачі, тому для опису семантики циклів потрібно свого роду "підказка" від розробника програми.

Найбільш відомим з методів доказу часткової коректності програм є метод індуктивних тверджень запропонований Флойдом і вдосконалений Хоаром. Метод складається з трьох етапів.

Перший етап - отримання анотованої програми. На цьому етапі для синтаксично правильної програми повинні бути задані твердження на мові логіки предикатів першого порядку:

6

вхідний предикат;

вихідний предикат;

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

Доказ неістинності умов коректності свідчить про неправильність програми, або її специфікації, або програми і специфікацій.

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

ЦЕЛІ, ПРІНЦИПИ І ЕТАПИ ТЕСТУВАННЯ

Кожному програмісту відомо, скільки часу і сил йде на відладку і тестування програм. На цей етап доводиться біля 50% загальної вартості розробки програмного забезпечення.

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

Інше визначення тестування ( у м. Майерса ) тестування - це процес виконання програми з метою виявлення в ній помилок. Таке визначення мети стимулює пошук помилок в програмах. Звідси також ясно, що “вдалим" тестом є такою, на якому виконання програми завершилося з помилкою. Навпаки, “невдалим можна назвати тест, що не дозволив виявити помилку в програмі.

Визначення м. Маєрса вказує на об'єктивну трудність тестування: це деструктивний ( тобто зворотний творчому ) процес. Оскільки програмування - процес конструктивний, ясно, що більшості розробників програмних засобів складно “перемкнутися" при тестуванні створеної ними продукції.