2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение) (1185699)

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

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

Распределенные алгоритмы.

Домашнее задание

Выполнили: Гуськов Дмитрий, Запутляев Иван, Савков Борис,

521 группа

Теорема:

Алгоритм возвращения кредита является корректным алгоритмом обнаружения завершения вычислений.

Доказательство:

1. С учетом правил П₁-П₅ и утверждений S₁-S₃, утверждение является инвариантом алгоритма возвращения кредита, где:

Алгоритм завершается (то есть завершение вычислений будет обнаружено) при ret=1. Это значит, что предикат term( )=True, где – заключительная конфигурация, в которой не может произойти ни одного базового события.

2. Обоснование корректности инварианта:

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

2) Рассмотрим состояние системы в этот момент:

• По определению предиката term все процессы p находятся в состоянии passive, а значит, в силу утверждения S₃, для всех процессов p: cred_p=0

• По определению предиката term в каналах отсутствуют сообщения

• По определению заключительной конфигурации в каналах отсутствуют сообщения

3) В итоге:

и завершение вычислений будет обнаружено.

Корректность инварианта обоснована. Теорема доказана.

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

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

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

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

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

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