Задания для самостоятельной работы
На одном из языков программирования напишите программу по предлагаемым ниже вариантам, расставьте индуктивные утверждения и и докажите ее правильность..(Блок-схемы программ приведены в [4] – рис. 2.3 – 2.5).
1. Вычисление произведения M на N при условии, что знак умножения использовать нельзя, M и N имеют целые значения и M ³ 0
2. Вычисление и печать значения M N при условии, что M и N имеют целые значения и M ³ 1, N ³ 1,
3. Вычисление и печать значения M! = 1 × 2 × 3 × ... × (M – 1) × M при условии, что в качестве M вводится положительное целое,
4. Поиск минимального элемента одномерного массива.
3.3. Контрольные вопросы к защите Лабораторной работы №3
Тема1 «Доказательство правильности программ»
1. Можно ли применять для доказательства правильности программ математическую индукцию?
2. Можно ли применять метод индуктивных утверждений для доказательства правильности программ?
3. Как в программе записываются индуктивные утверждения?
4. Назовите 3 основных отличия доказательства правильности программ от доказательства правильности блок-схем.
Глава 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 !
Далее мы докажем, что 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.]
= 4 [Так как X1 = 0 истинно, следовательно,
А(0, 3) = 3 + 1=4.]
Из этого примера следует, что при выполнении вычислений для рекурсивной программы мы можем сталкиваться с неоднозначностями, которые требуют уточнений. Например, в приведенных вычислениях при обращении А(0, А(1, 1)) мы предполагаем, что А(1, 1) должно быть вычислено прежде, чем мы продолжим вычисления, относящиеся к внешнему обращению к А. Если отдать предпочтение вычислениям, связанным с внешним обращением, то вычисления должны были бы идти в следующем порядке:
А(1, 2) = А(0, А(1, 1)) = А(1, 1) + 1 = А(0, А(1, 0)) + 1 =
= (А(1, 0) + 1) + 1 = (А(0, 1) + 1) + 1 = (2 + 1) + 1=4.
Значение А(1, 2) остается тем же, хотя последовательность вычислений отлична от предыдущей. Можно доказать, что если к одним и тем же аргументам некоторой рекурсивной функции применять две различные последовательности ее вычисления, то результат будет одним и тем же при условии конечности этих последовательностей. Однако вполне возможно, что одна последовательность не будет заканчиваться, хотя другая последовательность закончится. Рассмотрим следующий пример.
Пример 4.3. Возьмем рекурсивную программу, применимую к любой паре неотрицательных целых X1, Х2:
F(Х1, Х2) º IF X1 =0 ТНЕN 0
ELSE OTHERWISE F(0, F(Х1, Х2))
Проследим за вычислением F(1, 1), используя два различных правила вычислений. По первому правилу мы будем стараться сначала заканчивать вычисления, относящиеся к внешнему обращению. По второму правилу мы будем отдавать предпочтение самому внутреннему обращению:
1) F(1, 1) = F(0, F(1, 1)) [Так как условие X1 = 0 ложно.]
= 0 [Так как условие X1 = 0 истинно
для внешнего обращения к F.]
2) F(1, 1) = F(0, F(1, 1)) [Так как условие X1 = 0 ложно.]
= F(0, F(0, F(1, 1))) [Так как условие X1 = 0 для
внутреннего обращения ложно.]
= F(0, F(0, F(0, F(1, 1)))) =
= F(0, F(0, F(0, F(0, F(1,1))))) и т. д.
Таким образом, в первом случае последовательность вычислений F(1, 1) конечна и F(1, 1) = 0. Во втором случае вычисления не заканчиваются и, следовательно, значение F(1, 1) не определено. Однако отметим, что если для каких-либо аргументов в обоих случаях вычисления заканчиваются, то результат будет одним и тем же. Например, F(0, М) = 0 независимо от применяемых правил вычислений.
Итак, чтобы сделать наш язык программирования точным, нам нужно задать правила вычислений для программ, определяющие последовательность вычислений. В данной главе мы будем считать, что правило вычислений отдает предпочтение самому левому и самому внутреннему обращению. Другими словами, в любой из моментов вычислений первым начинает вычисляться левое и внутреннее обращение (для простоты далее везде будем опускать слово «самое») к функции F, все аргументы которой уже не содержат F. Это правило – не обязательно наилучшее, иногда оно может приводить к неоканчивающейся последовательности вычислений, хотя другое правило дало бы конечную последовательность (пример 4.3). Однако во многих существующих языках программирования используется правило вычислений, подобное описанному выше. Кроме того, как мы уже отмечали, если, следуя этому правилу, вычисления заканчиваются, то результат будет тем же, что и при других правилах, приводящих к окончанию. Большинство рассматриваемых нами программ заканчивается при любых значениях аргументов независимо от того, какие правила вычислений мы используем, а следовательно, и результат в любых случаях будет одинаковым. Однако для определенности все же будем считать, что предпочтение отдается левому внутреннему обращению.
Многие из приводимых в этой главе примеров относятся к работе со списками. В таких программах мы используем некоторое подобие «лисповской» нотации. По этой нотации список – набор объектов, отделенных друг от друга пробелами и заключенных в квадратные скобки [ ]. Объектами, входящими в такие списки, являются атомы или другие списки. Атом – строка буквенно-цифровых символов, не содержащая пробелов. Мы будем считать, что атомы должны начинаться с одной из букв А, В, С, D или F, а переменные – с букв, отличных от этих букв. Такой прием позволяет нам при написании программ различать переменные и атомы и обходиться без более общей функции Quote, используемой в Лиспе. Например, [А В С] – список из трех элементов, каждый из которых есть атом; [А [В А [С]] В С] – список, в котором (на верхнем уровне) четыре элемента. Второй элемент – сам список [В А [С]]. Третий элемент этого списка – опять список [С]. Для пустого списка, т.е. списка, не содержащего ни одного элемента, мы выделяем специальное имя NIL. Кроме того, мы будем использовать следующие проверки и функции:
1. Проверка = может применяться как к спискам, так и к числам. Например, проверка [А В] = [А В] истинна, а проверки [А В] = [В А], [А В] = [А [В]], В = А, А = NIL ложны.
2. Проверка АТОМ (X) применима к любым объектам, будь то атомы или списки. АТОМ (X) дает значение TRUE (истина), если X – атом или пустой список. Если X – непустой список, то АТОМ (X) дает значение FALSE (ложь).
3. Функция CAR (L) применима к любому непустому списку. В качестве результата выступает первый (на верхнем уровне) элемент этого списка. Примеры:
CAR ( [А В С] ) дает А. CAR ( [[А В] С] ) дает [А В].
CAR (NIL) не определено. CAR (А) не определено.
4. Функцию CDR(L) можно применять к любому непустому списку. Результатом является список, полученный из L путем отбрасывания первого его элемента (на верхнем уровне). Примеры:
CDR ( [А В С] ) дает [В С]. CDR ( [[А В] С] ) дает [С].
CDR ( [В] ) дает NIL (или [ ] ). CDR (NIL) не определено.
CDR (А) не определено.
5. Функцию CONS(Х, L) можно применять к любому списку L и любому X, будь то атом или список. В результате получается новый список: первый его элемент есть X, а потом идут элементе списка L. Примеры:
CONS ( А, [В С] ) дает [А В С]. CONS (А, NIL) дает [А].
CONS ( [А В], [В [С]] ) дает [[А В] В [С]]. CONS (А, В) не определено.
В некоторых из наших примеров мы будем использовать и специальные атомы ТRUЕ и FALSE.
Пример 4.4. Как пример использования новой нотации приведем рекурсивную программу, определяющую, является ли X элементом списка L (на верхнем уровне):
МЕМВЕR (Х, L) º IF L = NIL ТНЕN FALSE
ЕLSЕ IF Х = САR (L) ТНЕN TRUE
ЕLSЕ ОТНЕRWISЕ МЕМВЕR (X, CDR (L))
Проследим, как идет процесс вычислений по такой программе для фактических аргументов С и [А В С D]:
МЕМВЕR (С, [А В С D] ) = МЕМВЕR (С, [В С D] )
= МЕМВЕR (С, [С В] ) = TRUЕ
Теперь проследим, как проходит вычисление при фактических аргументах С и [А В [С D]]:
МЕМВЕR (С, [А В [С D]]) = МЕМВЕR (С, [В [С D]] )
= МЕМВЕR (С, [[С В]] ) = МЕМВЕR (С, NIL) = FALSE
Пример 4.5. Напишем рекурсивную программу, добавляющую список L1 к списку L2, другими словами, в этом списке, состоящем из двух, элементы первого стоят перед элементами второго:
APPEND (L1, L2) º IF L1 = NIL ТНЕN L2
ЕLSЕ OTHERWISE CONS (CAR (L1),
АРРЕND (CDR(L1), L2))
Проследим, как идет процесс вычислений при различных парах аргументов:
АРРЕND ([А В], [С D]) = CONS (САR ([А В]), АРРЕND (CDR ([А В]), [С D]))) =
= СОNS (А, АРРЕND ([В], [С D] )) = СОNS (А, СОNS (CAR ([В]),
АРРЕND (CDR([В]), [С D]))) = CONS (А, СОNS (В, АРРЕND (NIL, [С D] ))) =
= СОNS (А, СОNS (В, [С, D])) = СОNS (А, [В С D]) = [А В С D]
АРРЕND ([[А]], [В С] ) = СОNS ([А], АРРЕND (NIL, [В С])
= СОNS ([А], [В С]) = [[А] В С]
АРРЕND([А В], NIL) = СОNS (А, АРРЕND ([В], NIL))
= СОNS (А, СОNS (В, АРРЕND (NIL, NIL)))
= СОNS (А, СОNS ( [В] ) = СОNS (А, [В] ) = [А В]
Структурная индукция
Рекурсивные программы обычно строятся по следующей схеме: сначала в них явно определяется способ вычисления результата для наипростейших значений аргументов рекурсивной функции, затем способ вычисления результата для аргументов более сложного вида, причем используется сведение к вычислениям с данными более простого вида (с аргументами рекурсивного обращения к той же функции). Таким образом, вполне естественно попытаться доказать правильность таких программ следующим образом:
1) доказать, что программа работает правильно для простейших данных (аргументов функции);
2) доказать, что программа работает правильно для более сложных данных (аргументов функции) в предположении, что она работает правильно для более простых данных (аргументов функции).
Такой способ доказательства правильности для рекурсивных функций естествен, поскольку он следует основной схеме вычислений в рекурсивных программах. Студенты уже, конечно, обратили внимание на то, что этапы 1 и 2 фактически являются этапами доказательства с помощью индукции, но индукция осуществляется «по структуре» данных, которые обрабатывает программа. В частности, если можно сопоставить интуитивное понятие более простых данных (допустимых аргументов функции) и более сложных с отношением во вполне упорядоченном множестве значений данных (допустимых аргументов функции), то этапы 1 и 2 будут аналогичны этапам доказательства правильности работы программы для всех допустимых аргументов с помощью метода обобщенной индукции. Предложенный выше способ доказательства правильности назовем доказательством с помощью структурной индукции. Проиллюстрируем этот метод на нескольких очень простых рекурсивных программах.
Пример 4.6. Докажем правильность программы (разд. 4.1, пример 4.1):
F(Х) º IF X = 1 ТНЕN 1
ЕLSЕ ОТНЕRWISЕ X•F(Х – 1)
Предполагается, что эта функция вычисляет факториал от аргумента. Нужно доказать, что F(М) = 1 • 2 • 3 • ... • N = N! для любого положительного числа N. При доказательстве с помощью структурной индукции используем простую индукцию по положительным целым числам:
1) докажем, что F(1)= 1!. Действительно, F(1)= 1=1!;
2) докажем (для любого положительного числа N), что если
F(М) = 1 • 2 • ... • N = N!, то F(N + 1) = 1 • 2 • ... • N • (N + 1) = (N + 1)!. Следовательно, мы предполагаем, что N – положительное число, а F(N) = N! – гипотеза индукции. Так как N положительное число, то проверка N + 1 = 1 дает отрицательный ответ, и, прослеживая далее последовательность вычислений, получаем
F(N + 1) = (N + 1) • F((N + 1) – 1) = (N + 1) • F(N) =
= (N +1) • (N!) = (N +1) • (1 • 2 • ... • N) = 1 • 2 • ... • N • (N +1) = (N +1)!
(По гипотезе индукции)
что и требовалось доказать, т. е. F(N) = N! для любого положительного числа N.
Пример 4.7. Докажем правильность программы (разд. 4.1, пример 4.4):
МЕМВЕR (Х, L) º IF L = NIL THEN FALSЕ
ЕLSЕ IF Х = CAR(L) ТНЕN TRUE
ЕLSЕ ОТНЕRWISЕ МЕМВЕR (X, CDR(L))
Эта программа применима для любого элемента X и любого списка L. Предполагается, что она дает значение ТRUЕ, если X входит в качестве элемента верхнего уровня в список L; в противном же случае она дает значение FALSЕ:
МЕМВЕR (Х, L¢) = TRUE, если X элемент списка L¢
= FALSЕ в других случаях.
Для доказательства правильности работы этой программы используем структурную индукцию. Анализ программы показывает, что при рекурсивном обращении к МЕМВЕR из третьей строки программы только второй аргумент обращения выглядит проще, чем ранее. Таким образом, естественно вести индукцию только по второму аргументу функции. При рекурсивном обращении к МЕМВЕR ее второй аргумент CDR (L) представляет собой список, который содержит на один элемент (на верхнем уровне) меньше, чем список L. Следовательно, в структурной индукции можно использовать простую индукцию по числу элементов в списке L. Так как это число всегда неотрицательно, то доказательство основывается на простой индукции по неотрицательным целым числам. Итак, нужно:
1) доказать, что для любого списка, содержащего нуль элементов, МЕМВЕR работает правильно. Поскольку список, имеющий нуль элементов, это просто пустой список NIL, то очевидно, что МЕМВЕR (Х, NIL) = FALSЕ, так как X не есть элемент списка NIL;
2) доказать (для любого целого числа N), что если программа МЕМВЕR правильно работает для всех списков L¢, содержащих N элементов (на верхнем уровне), то она будет правильно работать и для всех списков L, содержащих на верхнем уровне (N + 1) элементов. Поэтому предположим, что МЕМВЕR правильно работает для списков L¢ длиной N, т.е.
МЕМВЕR (Х, L¢) = TRUE если X есть элемент из L¢,
= FALSЕ в других случаях.
Это гипотеза индукции. Предположим, что L есть список, содержащий (N + 1) элементов. Поскольку (N + 1) ³ 1, то L ¹ NIL. Прослеживая выполнение функции, видим, что
МЕМВЕR (Х, L) = TRUE если X = CAR (L),
= МЕМВЕR (Х, CDR (L)) в других случаях.
Если X = CAR(L) (а мы знаем, что CAR(L) определено, так как L¹NIL), то X – элемент списка L, и, следовательно, значение TRUЕ есть именно то значение, которое требуется. Если Х ¹ CAR (L), то X будет элементом списка L, если и только если X будет элементом CDR (L). (Функция CDR (L) определена, так как L ¹ NIL.) Однако CDR (L) представляет собой список из N элементов, и по гипотезе индукции следует, что МЕМВЕR (Х, СDR (L)) будет правильно вычислять значение TRUE или FALSЕ в зависимости от того, является ли X элементом CDR (L) или нет. Таким образом, если Х ¹ CDR (L), то МЕМВЕR (Х, L) = МЕМВЕR (Х, CDR (L)), а последняя функция вычисляет значение либо TRUЕ, либо FALSЕ в зависимости от того, будет ли X элементом CDR (L), а следовательно, элементом списка L или нет, что и требовалось доказать.
Дата добавления: 2018-05-12; просмотров: 328; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!