/* {0 ≤ J1 Λ 1 ≤ J2} */
IQ=0;
IR=J1;
/* {J1= IQ ●J2 + IR Λ 0 ≤ IR} */
DО WHILE (IR ≥ J1);
IQ = IQ + 1;
IR = IR – J2;
END ;
/* {J1= IQ ●J2 + IR Λ 0 ≤ IR < J2} */
Мы хотим доказать, что {0 ≤ J1 Λ 1≤ J2} P {J1= IQ●J2 + IR Λ 0 ≤ IR < J2}, где Р – приведенный выше фрагмент программы. Для этого нам нужно доказать:
1. {0 ≤ J1 Λ 1 ≤ J2} ≡ {А1}
IQ=0;
IR=J1;
{J1= IQ ●J2 + IR Λ 0 ≤ IR} ≡ {А2}
Это очевидно, так как после выполнения двух операторов из этого фрагмента программы мы будем иметь IQ=0 и IR=J1, а поэтому справедливо J1= 0●J2 + J1 = J1. Кроме того, так как перед выполнением этих действий справедливо 0 ≤ J1 и значение J1 при этом не изменяется, то после их выполнения будет справедливо
0 ≤ J1 = IR.
2. {J1= IQ ●J2 + IR Λ 0 ≤ IR} ≡ {А2}
DО WHILE (IR ≥ J1);
IQ = IQ + 1;
IR = IR – J2;
END ;
{J1= IQ ●J2 + IR Λ 0 ≤ IR < J2} ≡ {А3}
Для доказательства этого положения воспользуемся правилом верификации, приведенным в примере 3.2. Из правила следует, что мы сможем сделать требуемое заключение, если докажем:
а) {А2 Λ IR ≥ J2}
IQ = IQ + 1
IR = IR – J2
{А2}
Пусть переменные перед выполнением этого фрагмента программы имели значения J1n, J2n, IQn и IRn. Таким образом, J1n=IQn●J2n + IRn и 0 ≤ IRn Λ 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 Λ 0 ≤ IR и ¬(IR ≥ J1) следует из J1= IQ ●J2 + IR Λ 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}
и, следовательно, по правилу верификации можно заключить, что требуемое утверждение справедливо:
IQ = IQ + 1
IR = IR – J2
DО WHILE (IR ≥ J1);
IQ = IQ + 1;
IR = IR – J2;
END;
{А3}≡ { J1= IQ ●J2 + IR Λ 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 применима программа, т. е. нужно задать область определения функции. Выполнение программы заключается в применении ее к некоторым конкретным данным из ее области определения.
Пример 4.1. Рассмотрим рекурсивную программу, определенную для любого положительного целого числа X:
F(Х) ≡ IF Х = 1 THEN 1
ELSE OTHERWISE X•F(Х–1)
Чтобы понять, как работает такая программа, выполним ее для некоторого конкретного значения аргумента X. Например,
F(4) = 4 • F(3) [Так как условие 4 = 1 ложно, то F(4)=4•F(3).
Теперь нужно вычислить F(3), т. е. рекурсивно
обратиться к F.]
= 4 • 3 • F(2) [Т. к. при вычислении F(3) условие 3=1 ложно,
то F(3) = 3•F(2).]
= 4 • 3 • 2 • F(1) [Так как условие 2 = 1 ложно, то F(2) = 2•F(1).]
= 4 • 3 • 2 • 1 [Так как условие 1 = 1 истинно, то F(1) = 1.]
= 24 = 4 !
В разд. 4.2 мы докажем, что F(Х) = Х! для любого положительного целого числа X.
Пример 4.2. Рассмотрим следующую рекурсивную функцию (функцию Аккермана), применимую для любой пары неотрицательных целых чисел X1, Х2:
А(Х1, Х2) ≡ IF X1 = 0 THEN Х2 + 1
ELSE IF Х2=0 THEN А(Х1–1, 1)
ELSE OTHERWISE А(Х1–1, А(Х1, Х2–1))
Проследим, как выполняется такая программа для некоторой пары X1 и Х2. Например,
А(1, 2) = А(0, А(1, 1)) [Так как условия X1 = 0 и Х2 = 0
ложны, необходимо вычислять А(1, 1) –
рекурсивное обращение.]
= А(0, А(0, А(1, 0))) [Так как условия X1 = 0 и Х2 = 0 ложны,
нужно вычислять А(1, 0).]
= А(0, А(0, А(0, 1))) [Так как условие X1 = 0 ложно,
а Х2 = 0 истинно.]
= А(0, А(0, 2)) [Так как X1 = 0 истинно,
следовательно, А(0, 1) = 1 + 1 = 2.]
= А(0, 3) [Так как X1 =0 истинно, следовательно,
А(0, 2) = 2 + 1 = 3.]
|
Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6 7 8 |
