грамування являє собою сукупність аксіом і правил висновку. За допомогою аксіом задається семантика простих операторів мови (привласнення, введення - виведення, виклику процедур). За допомогою правил висновку описується семантика складових операторів або керуючих структур (послідовності, умовного вибору, циклів). Серед цих правил висновку треба відмітити правило висновку для операторів циклу оскільки воно вимагає знання інваріанта циклу (формули, істинності якій не змінюється при будь-якому проходженні циклу). br/>
Побудова інваріанта для оператора циклу по його тексту є алгоритмічно не вирішуваної задачі, тому для опису семантики циклів потрібно свого роду "підказка" від розробника програми. p> Найбільш відомим з методів доказу часткової коректності програм є метод індуктивних тверджень запропонований Флойдом і вдосконалений Хоаром. Метод складається з трьох етапів. p> Перший етап - отримання анотованої програми. На цьому етапі для синтаксично правильної програми повинні бути задані твердження на мові логіки предикатів першого порядку:
6
вхідний предикат;
вихідний предикат;
по одному твердженням для кожного циклу (Ці твердження задаються для вхідної точки циклу і повинні характеризувати семантику обчислень в циклі). p> Доказ неістинності умов коректності свідчить про неправильність програми, або її специфікації, або програми і специфікації.
Незважаючи на достатню складність процесу верифікації програми і на те, що навіть успішно завершена верифікація не дає гарантій якості програми (так як помилка може міститися і у верифікації), застосування методів аналітичного доказу правильності дуже корисно для уточнення значення програми, а знання цих методів благотворно позначається на кваліфікації програміста.
Нарешті, динамічний контроль програми - це перевірка правильності програми при її виконанні на комп'ютері, тобто тестування.
ЦІЛІ, ПРИНЦИПИ І ЕТАПИ ТЕСТУВАННЯ.
Кожному програмісту відомо, скільки часу і сил пішов на налагодження і тестування програм. На цей етап припадає близько 50% загальної вартості розробки програмного забезпечення.
Але не кожен з розробників програмних засобів може вірно визначити мету тестування. Нерідко можна почути, що тестування - це процес виконання програми з метою виявлення в ній помилок. Але ця мета недосяжна: ні яке саме ретельне тестування не дає гарантії, що програма не містить помилок.
Інше визначення тестування (у м. Майерса) тестування - це процес виконання програми з метою виявлення в ній помилок. Таке визначення мети стимулює пошук помилок в програмах. Звідси також ясно, що "вдалим" тестом є такою, на якому виконання програми завершилося з помилкою. Навпаки, "невдалим можна назвати тест, що не дозволив виявити помилку в програмі. p> Визначення Г. Майерса вказує на об'єктивну трудність тестування: це деструктивний (тобто...
