Доказательство правильности программ (стр. 4 )

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

Рис. 3.2

Пример 3.2. Предположим, что мы используем язык, в котором есть оператор вида

DO WHILE (C)

S

END;

Смысл этого оператора полностью характеризуется приведенным на рис. 3.2 фрагментом блок-схемы. Если нужно доказать {А1} Р {А2} где Р – такой же цикл, как DО WHILE, то можно воспользоваться следующей аксиомой или правилом верификации: Если можно доказать, что

1) {А1 L С} S{А1}

и

2) из {А1 L Ø С} следует А2,

то отсюда можно заключить, что

3) {А1} P {А2}.

Эквивалентность этой аксиомы методу индуктивных утверждений очевидна, так как при доказательстве частичной правильности нашего фрагмента блок-схемы мы должны удостовериться, что:

1'. Если мы попали в точку 1 и справедливо утверждение А1 а затем проходим из точки 1 через точку 2 в точку 7, то снова справедливо утверждение А1. Но для этого пути нам известно, что до выполнения S справедливы и утверждение А1 и условие С. Мы стремимся показать, что если мы вновь попадем в точку 1 (т. е. выполнение S закончится), то А1 будет справедливым.

2.' Если мы попадем в точку 1 и справедливо условие А1, а затем проходим из точки 1 в точку 3, то А2 будет справедливо. Но для этого пути справедливо А1 и ложно условие С (т. е. Ø С справедливо). Мы стремимся показать, что из А1 и Ø С следует А2.

Следовательно, оба положения 1' и 2', которые нужно доказывать в методе индуктивных утверждений, фактически идентичны двум предусловиям 1 и 2, которые мы должны доказывать, если хотим использовать правило верификации.

Приведенное правило верификации иногда записывают в менее общей форме:

Если можно доказать, что

1) {А1 L С} S{А1},

то отсюда можно заключить, что

2) из {А1} P {А1 L Ø С}, где Р – цикл вида DO WHILE.

Студент может легко убедиться в справедливости такого варианта правила, а кроме того, и в том, что он, как и первый вариант, используется лишь для доказательства частичной правильности. Оба варианта не гарантируют, что Р когда-нибудь закончится.

Пример 3.3. Рассмотрим пример доказательства частичной правильности с помощью правил верификации. Для этого нам потребуется еще одно дополнительное правило. Предположим, что Р1, Р2 – два фрагмента программы и необходимо доказать некоторый факт, касающийся фрагмента, состоящего из Р1, за которым непосредственно следует Р2. В этом случае может оказаться полезным следующее правило верификации:

Если можно доказать, что

1) {А1} Р1 {А2}

и

2) {А2} Р2 {А3} ,

то отсюда можно заключить, что

3) {А1} Р1; Р2 {А3} .

В доказательстве мы будем использовать следующую запись:

{А1}

Р

{А2}.

Это то же самое, что и запись { А1}Р {А2}.

Докажем с помощью правил верификации частичную правильность программы на ПЛ/1, соответствующей блок-схеме, для которой мы уже доказали частичную правильность в примере 2.3 в первой части учебного пособия [2]. Студент может сравнить эти два дока­зательства и убедиться в их идентичности. Фрагмент программы имеет вид

/* {0 £ J1 L 1 £ J2} */

IQ=0;

IR=J1;

/* {J1= IQ ·J2 + IR L 0 £ IR} */

DО WHILE (IR ³ J1);

IQ = IQ + 1;

IR = IR – J2;

END ;

/* {J1= IQ ·J2 + IR L 0 £ IR < J2} */

Мы хотим доказать, что {0 £ J1 L 1£ J2} P {J1= IQ·J2 + IR L 0 £ IR < J2}, где Р – приведенный выше фрагмент программы. Для этого нам нужно доказать:

1. {0 £ J1 L 1 £ J2} º {А1}

IQ=0;

IR=J1;

{J1= IQ ·J2 + IR L 0 £ IR} º {А2}

Это очевидно, так как после выполнения двух операторов из этого фрагмента программы мы будем иметь IQ=0 и IR=J1, а поэтому справедливо J1= 0·J2 + J1 = J1. Кроме того, так как перед выполнением этих действий справедливо 0 £ J1 и значение J1 при этом не изменяется, то после их выполнения будет справедливо
0 £ J1 = IR.

2. {J1= IQ ·J2 + IR L 0 £ IR} º {А2}

DО WHILE (IR ³ J1);

IQ = IQ + 1;

IR = IR – J2;

END ;

{J1= IQ ·J2 + IR L 0 £ IR < J2} º {А3}

Для доказательства этого положения воспользуемся правилом верификации, приведенным в примере 3.2. Из правила следует, что мы сможем сделать требуемое заключение, если докажем:

а) {А2 L IR ³ J2}

IQ = IQ + 1

IR = IR – J2

{А2}

Пусть переменные перед выполнением этого фрагмента программы имели значения J1n, J2n, IQn и IRn. Таким образом, J1n=IQn·J2n + IRn и 0 £ IRn L IRn ³ J2n. После выполнения программы переменные примут следующие значения: J1n+1= J1n, J2n+1= J2n, IQn+1= IQn + 1, IRn+1= IRn – J2n,. Нужно показать, что J1n+1=
= IQn+1·J2n+1 + IRn+1 и 0 £ IRn+1. Это легко сделать, подставив в наше высказывание J1n+1, J2n+1, IQn+1 и IRn+1. После подстановки получим

J1n= (IQn + 1)·J2n + (IRn – J2n) = IQn·J2n + J2n + IRn – J2n =
= IQn·J2n + IRn и 0 £ IRn – J2n или J2n £ IRn.

Оба утверждения по нашему предположению должны быть справедливы.

б) Из А2 и Ø(IR ³ J1) следует А3, т. е. из J1= IQ ·J2 + IR L 0 £ IR и Ø(IR ³ J1) следует из J1= IQ ·J2 + IR L 0 £ IR < J1. Это очевидно, так как из J1= IQ ·J2 + IR следует J1= IQ ·J2 + IR, а из 0 £ IR и Ø(IR ³ J1) следует 0 £ IR < J1.

Таким образом, мы доказали:

1) {А1}

IQ = IQ + 1

IR = IR – J2

{А2}

2) {А2}
DО WHILE (IR ³ J1);

IQ = IQ + 1;

IR = IR – J2;

END;

{А3}

и, следовательно, по правилу верификации можно заключить, что требуемое утверждение справедливо:

3)  {А1} º {0 £ J1 L 1 £ J2}

IQ = IQ + 1

IR = IR – J2

DО WHILE (IR ³ J1);

IQ = IQ + 1;

IR = IR – J2;

END;

{А3}º { J1= IQ ·J2 + IR L 0 £ IR < J1}

рис. 3.3

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

В качестве упражнения представьте, что в используемом языке программирования есть оператор вида REPEAT S UNTIL С. Этот оператор имеет традиционный для языков программирования смысл: он эквивалентен приведенной на рис. 3.3 блок-схеме. Сформулируйте правило верификации для доказательства справедливости

{А1} REPEAT S UNTIL С{А2}.

Глава 4. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ
РЕКУРСИВНЫХ ПРОГРАММ

Во многих языках программирования разрешается писать рекурсивные программы, т. е. программы, в которых при вычислениях допускается обращение (рекурсивное) к самой себе аналогично тому, как обычная, нерекурсивная программа обращается к некоторой подпрограмме. Рекурсивные программы особенно удобны в тех случаях, когда речь идет о данных, структура которых определяется рекурсивно (например, списки или деревья). В языке Лисп, созданном специально для «нечисленных» вычислений на основе списков, понятие рекурсии является фундаментальным. В этой главе описаны методы, которые полезны при доказательстве правильности рекурсивных программ. Основной метод в таких доказательствах называется методом структурной индукции. Доказательство методом структурной индукции представляет собой доказательство с помощью математической индукции, но индукция осуществляется по структуре данных, с которыми работает программа.

Если студент незнаком с понятием рекурсии, он все равно сможет понимать излагаемый здесь материал. Мы не будем пользоваться каким-нибудь стандартным рекурсивным языком программирования, например Алголом или Лиспом, а «изобретем» упрощенный язык, которого нам будет достаточно, чтобы проиллюстрировать понятие рекурсии. В разд. 4.1 введен такой язык, в разд. 4.2 описан метод структурной индукции, а примеры рассмотрены в разд. 4.3. В разд. 4.4 показано, что метод структурной индукции может оказаться полезным и в тех случаях, когда речь идет о нерекурсивных программах. В частности, показано, что метод структурной индукции иногда легче использовать для доказательства правильности, чем метод индуктивных утверждении, если, например, речь идет о нерекурсивных программах, выполняющих рекурсивные по существу процессы, такие, как просмотр деревьев.

4.1. Упрощенный язык программирования
для иллюстрации понятия рекурсии

Упрощенный язык программирования нужен нам, чтобы ознакомить студентов с понятием рекурсии. Если студент знаком с рекурсией в каком-либо из существующих языков программирования, ему будет очень просто сопоставить наш упрощенный язык с соответствующими возможностями в этих реальных языках. Однако, если вы даже и незнакомы с понятием рекурсии из существующих языков, это не помешает вам понять содержание данного раздела.

Программа в нашем упрощенном языке программирования состоит из определения функции, заданного в виде

F(Х1, ... , ХN) º IF проверка 1 THEN выражение 1

ELSE IF проверка 2 THEN выражение 2

.

:

ELSE IF проверка m THEN выражение m

ELSE OTHERWISE выражение m + 1

Такая программа вычисляет значение F(Х1,... , ХN). Сначала выполняется проверка 1. Если проверка 1 дает ответ «истина», то значение функции есть значение выражения 1. Если проверка 1 дает ответ «ложь», то выполняется проверка 2. Если эта проверка дает ответ «истина», то значение функции есть значение выражения 2. Процесс идет таким образом до тех пор, пока не будет обнаружена первая из проверок (i-я), дающая значение «истина». Значение функции в этом случае есть значение выражения i. Если ни одна из проверок не окажется положительной, то значение функции есть значение выражения m + 1. Рекурсия вводится в этот язык программирования следующим образом: функция F, определяемая в нашей программе, может входить как часть в любое из выражений или проверок в программе. Такое появление F называется рекурсивным обращением к этой функции. Для каждой такой рекурсивной программы нужно еще указать, для каких значений аргументов X1, ... , ХN применима программа, т. е. нужно задать область определения функции. Выполнение программы заключается в применении ее к некоторым конкретным данным из ее области определения.