2016 Алгоритм Дейкстры-Шолтена_ корректность (подробное решение) (1185666)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Линь Данил, Шерварлы Валерия, 521 группа.

Теорема

Алгоритм Дейкстры-Шолтена является корректным алгоритмом обнаружения завершения вычисления; в нем используется M обменов контрольными сообщениями.

Доказательство (исходя из предположения, что для алгоритма доказан инвариант P)

Для доказательства корректности необходимо показать, что

1) если выполняется условие term, то алгоритм оповещения Announce будет вызван спустя конечное число шагов,

2) если вызван алгоритм Announce, то конфигурация удовлетворяет условию term.

Для обоснования условия 2 рассмотрим, когда вызывается процедура Announce. Из соотношения (4) инварианта P следует, что T (дерево вычисления, которое строит алгоритм) является деревом и процесс p₀ - его корень. Announce может быть вызвана либо из процедуры I_p, либо из процедуры A_p, причем только в том случае, если p = p₀ (условие if father_p = p). Также при этом обязательно счетчик вершин-последователей равен нулю (sc_p = 0) и состояние p₀ пассивное, p₀ удаляет сам себя из множества V_T вершин дерева T, корнем которого он являлся, следовательно дерево T остается пустым, и предикат term выполняется.

Докажем условие 1. Если выполняется предикат term, то все процессы пассивны и никакая очередь не содержит сообщений. В таком состоянии возможно только выполнение процедуры A_p, во время которой происходит получение одним из процессов контрольного сообщения sig и его счетчик последователей уменьшается на единицу. Так как количество контрольных сообщений и общее количество вершин-последователей таким образом постоянно уменьшается, то через конечное число шагов они станут равны нулю и алгоритм перейдет в заключительную конфигурацию, в которой дерево T является пустым. Это означает, что корень дерева - процесс p₀ - удалился из T, а согласно алгоритму перед этим будет запущена процедура Announce.

Рассмотрим общую сумму всех счетчиков последователей sc_p . Эта сумма каждый раз при отправлении базового сообщения увеличивается на единицу (в процедуре S_p), а при получении контрольного сообщения уменьшается на единицу (в процедуре A_p). При этом, когда алгоритм завершает работу, эта сумма равна нулю. Отрицательной она стать не может, согласно соотношению (3) в инварианте P о корректности подсчета вершин-последователей. Следовательно, количество контрольных сообщений равно M, то есть числу базовых вычислений.

Характеристики

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

Будьте внимательны на мобильных устройствах, так как там используются упрощённый функционал даже в официальном приложении от Microsoft, поэтому для просмотра скачивайте PDF-версию. А если нужно редактировать файл, то используйте оригинальный файл.

Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.

Список файлов курсовой работы