yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Різні конспекти лекцій->Содержание->4.10 Доказ правильності програм

Організація баз даних і знань

4.10 Доказ правильності програм

 

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

 Нехай P(X,Y) - програма, із заданими вхідними даними X і результатами Y. Предикат Q(X), визначений на вхідних даних, будемо називати предумовою програми P, а предикат R(X,Y), що пов'язує вхідні і вихідні змінні будемо називати постумовою програми P. Будемо також припускати, що в ході своєї роботи програма не міняє своїх вхідних змінних X.

Програма P(X,Y) коректна стосовно предумови Q(X) і постумови R(X,Y), якщо з істинності Q(X) до початку виконання програми необхідно, щоб, будучи запущеною, програма завершила свою роботу й по її завершенню предикат R(X,Y) буде істиною Умову коректності записують у вигляді тріади (тріади Хоора) - Q(X) {P(X,Y)} R(X,Y)

Вже з цього визначення стає ясно, що говорити про правильність треба не взагалі, а стосовно заданих специфікацій, наприклад, у вигляді предумови й постумови. Довести правильність тріади для складних програм, як уже зазначалось, досить складно. Один з методів (метод Флойда) полягає в тому, що програма розбивається на ділянки, розмічені предикатами - Q1, Q2, …QN, R... Перший із предикатів представляє предумову програми, останній - постумову. Тоді доказ коректності зводиться до доказу коректності послідовності тріад:

Q1{P1}Q2;               Q2{P2}Q3;           …QN{PN}R

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

 

 

55