Методи доведення правильності програм

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

Базові методи доказу. Відомо багато методів доказу специфікацій програм, деяким з них дамо короткий зміст.

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

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

Метод Хоара – це вдосконалений метод Флойда, заснований на аксіоматичному описі семантики мови програмування початкових програм. Кожна аксіома описує зміну значень змінних за допомогою операторів цієї мови. Формалізація операторів переходу і викликів процедур забезпечується за допомогою правил виводу, що містять індуктивні вислови для кожної точки і функції початкової програми.

Метод Маккарті полягає у структурній перевірці функцій, що працюють над структурними типами даних, структур даних і шляхів переходу під час символьного виконання програм. Ця техніка включає моделювання виконання коду з використанням символів для змінних даних. Тестова програма має вхідний стан, дані і умови її виконання.

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

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

Основу методу складає математична індукція, абстрактний опис програми і її обчислення. За допомогою цього методу можна довести істинність деякого припущення Р(n) залежно від параметра n для всіх n ³ n₀, і тим самим довести випадок Р (n₀). Виходячи з істинності Р(n) для будь-якого значення n, доводиться Р(n+1), що достатньо для доказу істинності Р(n) для всіх n ³ n₀.

Читайте також:

<== попередня сторінка	\|	наступна сторінка ==>
Концепторна мова специфікації	\|	Модель доказу програми за твердженнями

Не знайшли потрібну інформацію? Скористайтесь пошуком google:

Генерація сторінки за: 0.026 сек.