Контрольные вопросы

1. Язык проектирования программ PDL. Операторы выбора. Операторы цикла. Операторы описания данных. Операторы ввода/вывода и вызова процедур. Оператор leave. Предложения на естественном языке.

2. Нисходящее проектирование и нисходящая разработка.

3. Пошаговое совершенствование.

4. Восходящее проектирование.

5. Подыгрывающие программы (заглушки).

6. Структурное проектирование. Простая программа. Элементарная программа. Управляющие структуры, способы их описания.

7. Скалярные и агрегативные типы данных.

8. Массивы. Структуры. Списки. Очереди. Стеки. Множества. Графы. Деревья.

9. Абстрактные конструкции.

10. Фиксированные данные абстрактного типа.

11. Размещение указателей.

12. Защита данных от несанкционированного доступа.

5 Правильность программ

Одним из важных методов повышения эффективности проектирования программ является верификация программ или математическое доказательство того, что программа работает правильно. Для доказательства правильности программ используется аксиоматический подход, при котором применяется теория перечисления предикатов. Предполагается, что каждый оператор в программе выполняет заранее определенные действия, зависящие только от синтаксиса языка. Для двух предикатов P и Q и оператора S необходимо определить, истинно ли выражение:

«Если P истинно и если выполняется оператор S, то Q истинно».

Предикат P является спецификацией правильного выполнения оператора S, а предикат Q будет истинным после выполнения оператора S и является спецификацией следующего за S оператора.

Если это утверждение распространить на все операторы программы и если P является спецификацией первого оператора, а Q истинно после окончания программы, то будет доказана правильность всей программы относительно предикатов P и Q. Эту конструкцию можно записать в следующем виде:

где P называется предусловием истинности Q после выполнения программы S.

Доказательство правильности программы заключается в определении, является ли выражение {P}S{Q} истинным относительно входных спецификаций P, выходных спецификаций Q и операторов S программы. Если {P}S{Q} истинно, то это означает, что доказана правильность программы S относительно P и Q.

5.1 Аксиомы

Для целей доказательства правильности программ к правилам исчисления предикатов следует добавить правила, необходимые для выполнения последовательности операторов программы. Эти правила, называемые правилами следствия, формулируются следующим образом:

1) если {P}S{Q} и Q  R, то {P}S{R};

2) если {Q}S{R} и P  Q, то {P}S{R}.

Первое правило заключается в следующем: «Если P — предусловие для Q и если Q  R является теоремой исчисления предикатов, то P — предусловие для R». Таким образом, если P истинно и выполняется S, то R (так же, как и Q) истинно.

Второе правило следствия аналогично данному. Эти правила следствия можно представить в более формальном виде: числитель выражения является посылкой, а знаменатель — заключением:

1)

2)

Правила следствия используются для доказательства сложных элементов программы. Пусть программа представлена в виде структуры (рис. 5.1), где S_i — операторы, а P_i — предикаты, соответствующие дугам.

Рис. 5.1 — Структура программы

Предположим, что доказаны следующие утверждения: {P₁}S₁{P₁'} и {P₂}S₂{P₂'} для некоторых предикатов P₁' и P₂'. Если можно доказать, что P₁'  P₂ и P₂'  P₃, то, используя правила следствия, можно доказать, что {P₁}S₁;S₂{P₃} истинно.

Следует определить, какие операторы программы являются правильными. Предполагается, что программа состоит только из последовательности операторов присвоения и операторов if и do while.

Так как только оператор присвоения может изменять значение переменных, то для определения правильности оператора присвоения нужно добавить только одну аксиому, она называется аксиомой присвоения и формулируется следующим образом:

В соответствии с этой аксиомой устанавливается, что если P — утверждение, содержащее переменную x, истинно, то P должно быть истинно и до выполнения оператора присвоения, если x изменяется expr.

Например, если P(x) является предикатом x > 0 и x = x + 1 — оператор присвоения, то P(x + 1) является предикатом x + 1 > 0 или x > –1.

По правилам следствия, если можно доказать, что Q  P(x + 1) для некоторого предиката Q, то справедливо утверждение {Q}x = x + 1{x > 0} и предикат является предусловием для P.

Осталось определить правильные управляющие структуры. Введем следующие аксиомы.

Аксиома следования:

Два оператора программы могут быть объединены. Если после выполнения S₁ предикат Q остается истинным и Q есть предусловие для оператора S₂, то P является предусловием для операторов S₁; S₂.

Аксиома цикла:

Утверждается, что если истинность P не изменяется оператором S (т.е. является инвариантом), то P инвариантно относительно цикла, содержащего S. Кроме того, при выходе из цикла значение выражения B ложно.

Аксиома выбора:

а)

б)

Эти аксиомы устанавливают простые соотношения для оператора if.