Доказательство правильности алгоритма.
Математическая логика и теория алгоритмов
Содержание. 1. Постановка задачи. 2. Построение модели. 3. Описание алгоритма 4. Доказательство правильности алгоритма 5. Блок-схема алгоритма 6. Описание переменных и программа 7. Расчёт вычислительной сложности 8. Тестирование 9. Список литературы
Постановка задачи. Перечислить все способы расстановки n ферзей на шахматной доске n на n, при которых они не бьют друг друга.
Построение модели. Очевидно, на каждой из n горизонталей должно стоять по ферзю. Будем называть k-позицией (для k = 0, 1,...,n) произвольную расстановку k ферзей на k нижних горизонталях (ферзи могут бить друг друга). Нарисуем "дерево позиций": его корнем будет единственная 0-позиция, а из каждой k-позиции выходит n стрелок вверх в (k+1)-позиции. Эти n позиций отличаются положением ферзя на (k+1)-ой горизонтали. Будем считать, что расположение их на рисунке соответствует положению этого ферзя: левее та позиция, в которой ферзь расположен левее. Дерево позиций для n = 2
Данное дерево представлено только для наглядности и простоты представления для n=2. Среди позиций этого дерева нам надо отобрать те n-позиции, в которых ферзи не бьют друг друга. Программа будет "обходить дерево" и искать их. Чтобы не делать лишней работы, заметим вот что: если в какой-то k-позиции ферзи бьют друг друга, то ставить дальнейших ферзей смысла нет. Поэтому, обнаружив это, мы будем прекращать построение дерева в этом направлении. Точнее, назовем k-позицию допустимой, если после удаления верхнего ферзя оставшиеся не бьют друг друга. Наша программа будет рассматривать только допустимые позиции. Описание алгоритма. Разобьем задачу на две части: (1) обход произвольного дерева и (2) реализацию дерева допустимых позиций. Сформулируем задачу обхода произвольного дерева. Будем считать, что у нас имеется Робот, который в каждый момент находится в одной из вершин дерева. Он умеет выполнять команды:
вверх_налево (идти по самой левой из выходящих вверх стрелок) вправо (перейти в соседнюю справа вершину) вниз (спуститься вниз на один уровень)
вверх_налево вправо вниз
и проверки, соответствующие возможности выполнить каждую из команд, называемые "есть_сверху", "есть_справа", "есть_снизу" (последняя истинна всюду, кроме корня). Обратите внимание, что команда "вправо" позволяет перейти лишь к "родному брату", но не к "двоюродному". Будем считать, что у Робота есть команда "обработать" и что его задача - обработать все листья (вершины, из которых нет стрелок вверх, то есть где условие "есть_сверху" ложно). Для нашей шахматной задачи команде обработать будет соответствовать проверка и печать позиции ферзей. Доказательство правильности приводимой далее программы использует такие определения. Пусть фиксировано положение Робота в одной из вершин дерева. Тогда все листья дерева разбиваются на три категории: над Роботом, левее Робота и правее Робота. (Путь из корня в лист может проходить через вершину с Роботом, сворачивать влево, не доходя до нее и сворачивать вправо, не доходя до нее.) Через (ОЛ) обозначим условие "обработаны все листья левее Робота", а через (ОЛН) - условие "обработаны все листья левее и над Роботом".
Нам понадобится такая процедура: procedure вверх_до_упора_и_обработать {дано: (ОЛ), надо: (ОЛН)} begin {инвариант: ОЛ} while есть_сверху do begin вверх_налево end {ОЛ, Робот в листе} обработать; {ОЛН} end; Основной алгоритм: дано: Робот в корне, листья не обработаны надо: Робот в корне, листья обработаны {ОЛ} вверх_до_упора_и_обработать {инвариант: ОЛН} while есть_снизу do begin if есть_справа then begin {ОЛН, есть справа} вправо; {ОЛ} вверх_до_упора_и_обработать; end else begin {ОЛН, не есть_справа, есть_снизу} вниз; end; end; {ОЛН, Робот в корне => все листья обработаны}
Осталось воспользоваться следующими свойствами команд Робота (сверху записаны условия, в которых выполняется команда, снизу - утверждения о результате ее выполнения):
(1) {ОЛ, не есть_сверху} обработать {ОЛН} (2) {ОЛ} вверх_налево {ОЛ} (3) {есть_справа, ОЛН} вправо {ОЛ} (4) {не есть_справа, ОЛН} вниз{ОЛН}
Теперь решим задачу об обходе дерева, если мы хотим, чтобы обрабатывались все вершины (не только листья). Решение. Пусть x - некоторая вершина. Тогда любая вершина y относится к одной из четырех категорий. Рассмотрим путь из корня в y. Он может: а) быть частью пути из корня в x (y ниже x); б) свернуть налево с пути в x (y левее x); в) пройти через x (y над x); г) свернуть направо с пути в x (y правее x); В частности, сама вершина x относится к категории в). Условия теперь будут такими: (ОНЛ) обработаны все вершины ниже и левее; (ОНЛН) обработаны все вершины ниже, левее и над. Вот как будет выглядеть программа:
procedure вверх_до_упора_и_обработать {дано: (ОНЛ), надо: (ОНЛН)} begin {инвариант: ОНЛ} while есть_сверху do begin обработать вверх_налево end {ОНЛ, Робот в листе} обработать; {ОНЛН} end; Основной алгоритм: дано: Робот в корне, ничего не обработано надо: Робот в корне, все вершины обработаны {ОНЛ} вверх_до_упора_и_обработать {инвариант: ОНЛН} while есть_снизу do begin if есть_справа then begin {ОНЛН, есть справа} вправо; {ОНЛ} вверх_до_упора_и_обработать; end else begin {ОЛН, не есть_справа, есть_снизу} вниз; end; end; {ОНЛН, Робот в корне => все вершины обработаны} Приведенная только что программа обрабатывает вершину до того, как обработан любой из ее потомков. Теперь изменим ее, чтобы каждая вершина, не являющаяся листом, обрабатывалась дважды: один раз до, а другой раз после всех своих потомков. Листья по-прежнему обрабатываются по разу: Под "обработано ниже и левее" будем понимать "ниже обработано по разу, слева обработано полностью (листья по разу, остальные по два)". Под "обработано ниже, левее и над" будем понимать "ниже обработано по разу, левее и над - полностью".
Программа будет такой:
procedure вверх_до_упора_и_обработать {дано: (ОНЛ), надо: (ОНЛН)} begin {инвариант: ОНЛ} while есть_сверху do begin обработать вверх_налево end {ОНЛ, Робот в листе} обработать; {ОНЛН} end; Основной алгоритм: дано: Робот в корне, ничего не обработано надо: Робот в корне, все вершины обработаны {ОНЛ} вверх_до_упора_и_обработать {инвариант: ОНЛН} while есть_снизу do begin if есть_справа then begin {ОНЛН, есть справа} вправо; {ОНЛ} вверх_до_упора_и_обработать; end else begin {ОЛН, не есть_справа, есть_снизу} вниз; обработать; end; end; {ОНЛН, Робот в корне => все вершины обработаны полностью} Доказательство правильности алгоритма. Докажем, что приведенная программа завершает работу (на любом конечном дереве). Доказательство. Процедура вверх_налево завершает работу (высота Робота не может увеличиваться бесконечно). Если программа работает бесконечно, то, поскольку листья не обрабатываются повторно, начиная с некоторого момента ни один лист не обрабатывается. А это возможно, только если Робот все время спускается вниз. Противоречие. Блок-схема алгоритма.
Популярное: Как распознать напряжение: Говоря о мышечном напряжении, мы в первую очередь имеем в виду мускулы, прикрепленные к костям ... Почему человек чувствует себя несчастным?: Для начала определим, что такое несчастье. Несчастьем мы будем считать психологическое состояние... ©2015-2024 megaobuchalka.ru Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав. (270)
|
Почему 1285321 студент выбрали МегаОбучалку... Система поиска информации Мобильная версия сайта Удобная навигация Нет шокирующей рекламы |