рефераты конспекты курсовые дипломные лекции шпоры

Реферат Курсовая Конспект

Взаимодействующие последовательные процессы

Взаимодействующие последовательные процессы - раздел Программирование, Математические основы программирования. Теория схем программ. Семантическая теория программ Как Уже Отмечалось Во Введении, Наиболее Очевидной Сферой Применения Результа...

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

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

Во-вторых, он включает в себя в виде частных случаев модели структурного программирования: мониторы, классы, модули, пакеты, критические участки, конверты, формы и даже подпрограммы.

В-третьих, он является надежной основой для избежания таких ошибок, как расходимость, тупики, зацикливание.

3.1.1. Определения

Неформально, процесс можно представить себе как группу ячеек памяти, содержимое которых меняется по определенным правилам. В ЭВМ эти правила описываются программой, которую интерпретирует процессор. Синоним термина «Процесс», – «задача», «программа».

«Задача – основная единица, подчиняющаяся управляющей программе в мультипрограммном режиме»; «Процесс – это программа, выполняемая псевдопроцессором»; «Процесс – это то, что происходит при выполнении программы на ЭВМ».

Хорнинг и Ренделл (1973) построили формальное определение понятие процесса.

Основные термины модели:

- набор переменных состояния;

- состояние;

- пространство состояний;

- действия;

- работа;

- функция действия;

- процесс;

- начальное состояние.

В модели ВПП понятие процесс используется для обозначения поведения объекта. Для формального описания поведения объекта в ВПП необходимо сначала выделить в таком поведении наиболее важные события или действия, и выбрать для каждого из них подходящее название, или имя.

В случае простого автомата, торгующего шоколадками, существуют два вида событий;

мон - опускание монеты в щель автомата,

шок - появление шоколадки из выдающего устройства.

Заметим, что имя каждого события обозначает целый класс событий; отдельные вхождения события внутри одного класса разделены во времени. Множество имен событий, выбранных для конкретного описания объекта, называется его алфавитом.

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

Введем следующие соглашения:

  1. Имена событий будем обозначать словами, составленными из строчных букв, например, шок, а также буквами а, b, с...
  2. Имена процессов будем обозначать словами, составленными из прописных букв, например, ТАП — простой торговый автомат, а буквами Р, Q, R будем обозначать произвольные процессы.
  3. Буквы х, у, z используются для переменных, обозначающих события.
  4. Буквы А, В, С используются для обозначения множества событий.
  5. Буквы X, У используются для переменных, обозначающих процессы.
  6. Алфавит процесса Р обозначается aР, например, aТАП = {мон, шок}.
  7. Процесс с алфавитом V, такой, что в нем не происходит ни одно событие из V, назовем СТОПA. этот процесс описывает поведение сломанного объекта. Далее определим систему обозначений, которая также предназначена для описания поведения объектов.

3.1.1.1. Префиксы

Пусть х событие, а Р — процесс. Тогда (х ® Р) (читается как «Р за х») описывает объект, который вначале участвует в событии х, а затем ведет себя в точности как Р, где

a(х ® Р) = aР, x Î aР.

Пример 3.1. Простой торговый автомат, который благополучно обслуживает двух покупателей и затем ломается:

(мон ® (шок ® (мон ® (шок ® СТОПaТАП)))).

В дальнейшем скобки будут опускаться в случае линейной последовательности событий. Условимся, что операция → ассоциативна справа.

3.1.1.2. Рекурсия

Префиксную запись можно использовать для полного описания поведения процесса, который рано или поздно останавливается. Было бы желательно, чтобы этот способ был компактным и не требовал знать заранее срок жизни объекта.

Рассмотрим простой долговечный объект — часы, функционирование которых состоит в том, чтобы тикать.

aЧАСЫ = {тик}.

Теперь рассмотрим объект, который вначале издает единственный «тик», а затем ведет себя в точности как ЧАСЫ

(тик®ЧАСЫ).

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

ЧАСЫ = (тик®ЧАСЫ).

Это уравнение можно развертывать простой заменой в правой части уравнения члена ЧАСЫ на равное ему выражение (тик®ЧАСЫ) столько раз, сколько нужно, при этом возможность для дальнейшего развертывания сохраняется. Мы эффективно описали потенциально бесконечное поведение объекта ЧАСЫ, как

тик ® тик ® тик ®…

Рекурсивный метод определения процесса, будет правильно работать, только если в правой части уравнения рекурсивному вхождению имени процесса предшествует хотя бы одно событие. Например, рекурсивное «определение» Х = Х не определяет ничего, так как решением этого уравнения может служить все что угодно. Описание процесса, начинающееся с префикса, называется предваренным.

Утверждение 3.1.Если F(Х) предваренное выражение, содержащее имя процесса X, а V — алфавит X, то уравнение Х = F(Х) имеет единственное решение в алфавите V.

Иногда обозначают это решение выражением

mХ: V.F(Х).

Пример 3.2.Простой торговый автомат, полностью удовлетворяющий спрос на шоколадки:

ТАП = (мон ® (шок ® ТАП)).

Решение этого уравнения может быть записано в виде ТАЛ = mХ: {мон, шок}.(мон ® (шок ® X)).

Утверждение о том, что предваренное уравнение имеет решение, и это решение единственное, можно неформально доказать методом подстановки. Всякий раз, когда в правую часть уравнения производится подстановка на место каждого вхождения имени процесса, выражение, определяющее поведение процесса, становится длиннее, а значит, описывает больший начальный отрезок этого поведения. Таким путем можно определить любой конечный отрезок поведения процесса. А так как два объекта, ведущие себя одинаково вплоть до любого момента времени, ведут себя одинаково всегда, то они представляют собой один и тот же процесс.

3.1.1.3. Выбор

Используя префиксы и рекурсию, можно описывать объекты, обладающие только одной возможной линией поведения. Однако поведение многих объектов зависит от окружающей их обстановки. Например, торговый автомат может иметь различные щели для 1- и 2-пенсовых монет; выбор одного из двух событий в этом случае предоставлен покупателю.

Если х и y — различные события, то (х ® P | у ® Q) описывает объект, который сначала участвует в одном из событий x, у, где a(х ® P | у ® Q) = aP, x, y Î aР и aР = aQ. Последующее же поведение объекта описывается процессом Р, если первым произошло событие х, или Q, если первым произошло событие y.

Пример 3.3. Процесс копирования состоит из следующих событий:

вв.0считывание нуля из входного канала,

вв.1 считывание единицы из входного канала,

выв.0запись нуля в выходной канал,

выв.1 — запись единицы в выходной канал.

Поведение процесса состоит из повторяющихся пар событий. На каждом такте он считывает, а затем записывает один бит.

КОПИБИТ=mХ: (вв.0 ® выв.0 ® X | вв.1 ® выв.1 ® X).

Определение выбора легко обобщить на случай более чем двух альтернатив. В общем случае если В - некоторое множество событий, а Р(х) - выражение, определяющее процесс для всех различных х из В, то запись

(х: В ® Р(х))

определяет процесс, который сначала предлагает на выбор любое событие у из В, а затем ведет себя как Р(у).

3.1.1.4. Взаимная рекурсия

Рекурсия позволяет определить единственный процесс как решение некоторого единственного уравнения. Эта техника легко обобщается на случай решения систем уравнений с более чем одним неизвестным. Для достижения желаемого результата необходимо, чтобы правые части всех уравнений были предваренными, а каждый неизвестный процесс входил ровно один раз в правую часть одного из уравнений.

Пример 3.4.Автомат с газированной водой имеет рукоятку с двумя возможными положениями — ЛИМОН и АПЕЛЬСИН. Действия по установке рукоятки в соответствующее положение назовем устлимон и устапельсин, а действия автомата по наливанию напитка — лимон и апельсин. Вначале рукоятка занимает некоторое нейтральное положение, к которому затем уже не возвращается. Ниже приводятся уравнения, определяющие алфавит и поведение трех процессов:

aАГАЗ = aG = aW = {устлимон, устапельсин, мон, лимон, апельсин}.

АГАЗ = (устлимон ® G | устапельсин ® W),

G = (мон ® лимон ® G | устапельсин ® W),

W = (мон ® апельсин ® W | устлимон ® G).

3.1.2. Законы

Тождественность процессов с одинаковыми алфавитами можно устанавливать с помощью алгебраических законов, очень похожих на законы арифметики.

Первый закон касается оператора выбора. Он гласит, что два процесса, определенные с помощью оператора выбора, различны, если на первом шаге они предлагают различные альтернативы или после одинакового первого шага ведут себя по-разному. Если же множества начального выбора оказываются равными и для каждой начальной альтернативы дальнейшее поведение процессов совпадает, то, очевидно, что процессы тождественны.

L1. (х: А ® Р(х)) = (у: В ® Q(у)) º (А = В AND "х Î А.Р(х) = Q(х))

Этот закон имеет ряд следствий:

L1A. СТОП ¹ (a ® P).

Доказательство: ЛЧасть = (х: {} ® P) ¹ (х: {a} ® Р) = ПРЧасть, так как {} ¹ {a}.

L1B. (с ® Р) ≠ ( d® Q), если с ≠ d.

Доказательство: Так как, {с} ≠ {d}.

L1C. (с ® Р | d® Q) = (d ® Q | с ® Р).

L1D. (с ® Р) = (с ® Q) º Р = Q.

Доказательство: Так как, {с} = {с}.

С помощью этих законов можно доказывать простые теоремы.

Пример 3.5. (мон ® шок ® мон ® шок ® СТОП) ¹ (мон ® СТОП).

Доказательство: Следует из L1B и L1A.

Для доказательства более общих теорем о рекурсивно определенных процессах необходимо ввести закон, гласящий, что всякое должным образом предваренное рекурсивное уравнение имеет единственное решение.

L2. Если F(X) — предваренное выражение, то (Y = F(Y)) º (Y = mX.F(X)).

Как прямое следствие получаем, что mX.F(X) является решением соответствующего уравнения

L2A.mX.F(X) = F(mX.F(X)).

Пример 3.6. Пусть ТА1 = (мон ® ТА2), а ТА2 = (шок ® ТА1). Требуется доказать, что ТА1 = ТАП.

Доказательство: ТА1 = (мон ® ТА2) = по определению ТА1

= (мон ® (шок ® ТА1)) по определению ТА2

Таким образом, ТА1 является решением того же рекурсивного уравнения, что и ТАП. Так как это уравнение предварённое, оно имеет единственное решение. Значит, ТА1 = ТАП.

3.1.3. Реализация процессов

Любой процесс Р, записанный с помощью введенных обозначений, можно представить в виде

(х: В ® F(х)).

где Fфункция, ставящая в соответствие множеству символов множество процессов. Множество В может быть пустым (в случае P = СТОП), может содержать только один элемент (в случае префикса) или — более одного элемента (в случае выбора).

Таким образом, каждый процесс можно рассматривать как функцию F с областью определения В (множество начальных событий), и областью значения {F(х) | x Î B}.

Такой подход позволяет представить любой процесс как функцию в некотором подходящем функциональном языке программирования, например в ЛИСПе. Каждое событие из алфавита процесса представлено атомом ("МОН"). При этом если символ не может быть начальным событием процесса, то результатом функции будет специальный символ "BLEEP". Например, для процесса (х: {} ® СТОП(х)) значением функции будет "BLEEP", что обозначим

СТОП = lx. "BLEEP".

Если же аргумент является событием, возможным для процесса, результатом функции будет другая функция, определяющая последующее поведение процесса.

Пример 3.7.Функция, реализующая процесс (c ® Р) может иметь вид:

префикс(c, Р) = lх. if x = с thenР else "BLEEP".

Пример 3.8.Функция, реализующая двуместный выбор (c ® Р | d ® Q) может иметь вид:

выбор(c, d, Р, Q) = lх. if x = с then Р else if x = d then Q else "BLEEP".

Оказывается возможным прямое кодирование рекурсивных уравнений:

Пример 3.9. ТАП = префикс("МОН", префикс("ШОК", ТАП)).

3.1.4. Протоколы

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

Будем обозначать протокол последовательностью символов, разделенной запятыми и заключенной в угловые скобки, например, протокол <х, у> состоит из двух событий — х и следующего за ним у, <x> - cостоит из одного события х, а протокол <> - пустой протокол.

Пример 3.10. Протокол простого торгового автомата ТАП в момент завершения обслуживания первых двух покупателей:

<мон, шок, мон, шок>.

Протокол того же автомата перед тем, как второй покупатель вынул свою шоколадку:

<мон, шок, мон>.

3.1.5. Операции над протоколами

Протоколам принадлежит основная роль в фиксировании, описании и понимании поведения процессов. В этом разделе мы исследуем некоторые общие свойства протоколов и операций над ними. Введем следующие обозначения:

s, t, u - протоколы,

S, Т, U - множества протоколов,

f, g, h – функции.

3.1.5.1. Конкатенация

Наиболее важной операцией над протоколами является конкатенация s^t, которая строит новый протокол из пары протоколов s и t, просто соединяя их в указанном порядке. Например,

<мон, шок>^<мон> = <мон, шок, мон>.

Самые важные свойства конкатенации — это ее ассоциативность и то, что пустой протокол <> служит для нее единицей:

L1.s^<> = <>^s.

L2. s^(t^u) = (s^t)^u.

Пусть f функция, отображающая протоколы в протоколы. Будем говорить, что функция строгая, если она отображает пустой протокол в пустой протокол: f(<>)=<>.

Будем говорить, что функция f дистрибутивна, если f(s^t) = f(s)^f(t).

Все дистрибутивные функции являются строгими.

Если n натуральное число, то tn будет обозначать конкатенацию n копий протокола t. Отсюда следует:

L3. tn+1= t^tn.

L4. (s^t)n+1 = s^(t^s)n^t.

3.1.5.2. Сужение

Выражение (t ­ А) обозначает протокол t, суженный на множество символов А; он строится из t отбрасыванием всех символов, не принадлежащих А.

Сужение дистрибутивно и поэтому строго.

L1. <> ­ A = <>.

L2. (s^t) ­ A = (s ­ A)^(t ­ A).

Эффект сужения на одноэлементных последовательностях очевиден:

LЗ. <х> ­ А = <х>, если х Î А.

L4. <y> ­ А = <>, если y Ï А.

Приведенные ниже законы раскрывают взаимосвязь сужения ­ и операций над множествами.

L5. s ­ {} = <>.

L6. (s ­ A) ­ B = s ­ (A Ç B).

3.1.5.3. Голова и хвост

Если s — непустая последовательность, обозначим ее первый элемент s0, а результат, полученный после его удаления — s’. Например, <x, y, х>0 = x, <х, у, х>' = y. Обе эти операции не определены для пустой последовательности.

L1. (<x>^s)0 = х.

L2. (<x>^s)’ = s.

L3. s = (<s0>^s’ ), если s ¹ <>.

Следующий закон предоставляет удобный метод доказательства равенства или неравенства двух протоколов:

L4. s = t º (s = t = <> OR (s0 = t0 AND s’ = t’)).

3.1.5.4. Звёздочка

Множество А* — это набор всех конечных протоколов (включая <>), составленных из элементов множества А. После сужения на А такие протоколы остаются неизменными, Отсюда следует простое определение:

А* = {s | (s ­ A) = s}.

Приведенные ниже законы являются следствиями этого определения:

L1. <> Î А*.

L2. <x> Î А* º x Î А.

L3. (s^t) Î А* º s Î А* AND t Î А*.

Они обладают достаточной мощностью, чтобы определить, принадлежит ли протокол множеству А*. Например, если х Î А, а y Ï А, то

<x, y> Î А* º (<x>^<y>) Î А*

º (<x> Î А*) AND(<y> Î А*) по L3

º T AND F = F по L2.

3.1.5.5. Порядок

Если s — копия некоторого начального отрезка t, то можно найти такое продолжение и последовательности s, что s^и = t. Поэтому мы определим отношение порядка

s £ t = ($u.s^и = t).

и будем говорить, что s является префиксом t. Например:<х, у> £ <х, у, z>. Отношение £ является частичным упорядочением и имеет своим наименьшим элементом <>. Об этом говорят законы

L1. <> £ s наименьший элемент.

L2. s £ s рефлексивность.

L3. s £ t AND t £ s Þ t = s антисимметричность.

L4. s £ t AND t £ u Þ s £ u транзитивность.

Следующий закон вместе сL1 позволяет определить, является ли справедливым отношение s £ t:

L5. (<x>^s) £ t º t ¹ <> AND x = t0 AND s £ t’.

Будем говорить, что функция f из множества протоколов во множество протоколов монотонна, если она сохраняет отношение порядка £, т. е. f(s) £ f(t) всякий раз, когда s £ t.

3.1.5.6. Длина

Длину протокола t будем обозначать #t. Например, #<х, у, z> = 3.

Следующие законы определяют операцию #:

L1. #<> = 0.

L2. #<x> = 1.

L3. #(s ^t) = #s + #t.

Число вхождений символа х в протокол s определяется как s ¯ х = #(s ­ {х}).

3.1.6. Протоколы процесса

Понятие протокола введено, как последовательная запись поведения процесса вплоть до некоторого момента времени. До начала процесса неизвестно, какой именно из возможных протоколов будет реализован: его выбор зависит от внешних по отношению к процессу факторов. Однако полный набор всех возможных протоколов процесса Р может быть известен заранее. Введем функцию протоколы(Р) для обозначения этого множества.

Пример 3.11. Единственным протоколом процесса СТОП является <>: протоколы(СТОП) = {<>}.

Пример 3.12. протоколы(ЧАСЫ) = {<>, <тик>, <тик, тик>,…} = {тик}*.

Здесь множество протоколов бесконечно.

3.1.6.1. Законы

В этом разделе покажем, как вычислить множество протоколов процесса, определенного с помощью уже введенных обозначений.

L1.протоколы(СТОП) = {t | t = <>} = {<>}.

Протокол процесса (с ® Р) может быть пустым, поскольку <> является протоколом поведения любого процесса до момента наступления его первого события.

L2. протоколы(с ® Р) = {t | t = <> OR (t0 = c AND t' Î протоколы(Р))}

= {<> È {<c>^t | t Î протоколы(Р)}.

Эти два закона можно объединить в один общий закон, которому подчиняется конструкция выбора:

LЗ. протоколы(x: B ® Р(x)) = {t | t = <> OR (t0 Î В AND t' Î протоколы(Р(t0)))}.

Несколько сложнее найти множество протоколов рекурсивно определенного процесса. Рекурсивно определенный процесс является решением уравнения Х = F(Х).

L4.протоколы(mХ: А.F(Х)) = Èn³0протоколы(Fn(СТОПA)).

Пример 3.13. протоколы(ТАП) = Èn³0{s | s £ <мон, шок>n}.

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

1) Согласно предположению индукции протоколы(Fn(ТAП)) = {t | t £ <мон, шок>n},

где F(X) = (мон ® шок ® X).

2) протоколы(F0(СТОП)) = {<>} = {s | s £ <мон, шок>0}, для n = 0 предположение выполняется.

3) Покажем, что предположение также справедливо для n+1:

протоколы(Fn+1(СТОП)) = протоколы(мон ® шок ® Fn(СТОП)) =

= {<>, <мон>} È {<мон, шок>^t | t Î протоколы(Fn(СТОП))} =

= {<>, {<мон>} È {<мон, шок>^t | t £ <мон, шок>n} =

= {s | s = <> OR s = <мон> OR $t.s = <мон, шок>^t AND t £ <мон, шок>n} =

= {s | s £ <мон, шок>n+1}.

Справедливо, что <> является протоколом любого процесса до момента наступления его первого события. Кроме того, если (s^t) – протокол процесса до некоторого момента, то s должен быть протоколом того же процесса до некоторого более раннего момента времени. Наконец, каждое происходящее событие должно содержаться в алфавите процесса. Три этих факта находят свое формальное выражение в следующих законах:

L5. <> Î протоколы(P).

L6. s^t Î протоколы(P) Þ s Î протоколы(P).

L7. протоколы(P) Í {aP}*.

3.1.6.2. После

Если s Î протоколы(P), то P/s (P после s)это процесс, ведущий себя так, как ведет себя Р с момента завершения всех действий, записанных в протоколе s. Если s не является протоколом P, то P/s не определено.

Пример 3.14.(ТАП / <мон>) = (шок → ТАП).

3.1.7. Спецификации

Спецификация изделия – это описание его предполагаемого поведения. Это описание представляет собой предикат, содержащий свободные переменные, каждая из которых соответствует некоторому обозримому аспекту поведения изделия.

Например, спецификация электронного усилителя с входным диапазоном в один вольт и с усилением входного напряжения приблизительно в 10 раз задается предикатом

УСИЛ10 = (0 £ v £ 1 Þ |v' - 10´v | £ 1).

В этой спецификации v обозначает входное, а v'- выходное напряжения.

В случае процесса наиболее естественно в качестве результата наблюдения за его поведением рассматривать протокол событий, произошедших вплоть до данного момента времени. Для обозначения произвольного протокола процесса будем использовать специальную переменную пр.

Пример 3.15. Владелец торгового автомата не желает терпеть убытков. Поэтому он оговаривает, что число выданных шоколадок не должно превышать числа опущенных монет:

НЕУБЫТ = (#(пр ­ {шок}) £ #(пр ­ {мон})) = пр ¯ шок £ пр ¯ мон. (см. 3.1.5.6.)

Пользователь автомата хочет быть уверенным в том, что машина не будет поглощать монеты, пока не выдаст уже оплаченный шоколад:

ЧЕСТН = (пр ¯ мон £ (пр ¯ шок + 1)).

Изготовитель торгового автомата должен учесть требования, как владельца, так и клиента:

ТАПВЗАИМ = ТАПНЕУБЫТ AND ЧЕСТН = (0 £ (пр ¯ монпр ¯ шок) £ 1).

3.1.7.1. Соответствие спецификации

Если Р - объект, отвечающий спецификацииS, то говорят, что Р удовлетворяет S, сокращенно

Р уд S.

Это означает, что S описывает все возможные результаты наблюдения за поведением Р, или, другими словами, S истинно всякий раз, когда его переменные принимают значения, полученные в результате наблюдения за объектом Р, или, более формально:

"пр.пр Î препротоколы(Р) Þ S.

В следующих законах приводятся наиболее общие свойства отношения удовлетворяет. Спецификации истина, не накладывающей никаких ограничений на поведение, будут удовлетворять все объекты.

L1. P уд истина.

Если объект удовлетворяет двум различным спецификациям, он удовлетворяет также и их конъюнкции:

L2А. Если Р уд S и Р уд Т, то Р уд (S AND T).

Пусть S(n) предикат, содержащий переменную n и Р не зависит от n.

L2B. Если "n.(Р уд S(n)), то Р уд "n.S(n).

Если из спецификации S логически следует другая спецификация T, то всякое наблюдение, описываемое S, описывается также и Т.

LЗ. Если Р уд S и S Þ T, то Р уд Т.

3.1.7.2. Доказательства

При проектировании изделия разработчик несёт ответственность за то, чтобы оно соответствовало своей спецификации. Эта ответственность может быть реализована посредством обращения к методам соответствующих разделов математики. В этом разделе мы приводим набор законов, позволяющих с помощью математических рассуждений убедиться в том, что процесс Р соответствует своей спецификации S.

Результатом наблюдения за процессом СТОП всегда будет пустой протокол:

L4А. СТОП уд (пр = <>).

Протокол процесса (с ® Р) вначале пуст. Каждый последующий протокол начинается с c, а его хвост является протоколом Р.

L4В. Если Р уд S(пр), то (с ® Р) уд (пр = <> OR (пр0 = c ANDS(пр'))).

Все приведенные выше законы являются частными случаями закона для обобщенного оператора выбора:

L5. Если "x Î B.(Р(x) уд S(пр, х)), то (х: В ® Р(x)) уд (пр = <> OR (пр0 Î B AND S(пр', пр0))).

Закон, устанавливающий корректность рекурсивно определенного процесса.

L6. Если F(X) — предваренная, СТОП уд S, а ((X уд S) Þ (F(Х) уд S)), то (mХ.F(Х)) уд S.

Пример 1.16. Докажем, что ТАП уд ТАПВЗАИМ.

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

1) СТОП уд (пр = <>) Þ 0 £ (пр ¯ монпр ¯ шок) £ 1), т.к. (<> ¯ мон = (<> ¯ шок) = 0.

Это заключение сделано на основании применения законов L4A и LЗ.

2) Предположим, что Х уд (0 £ ((пр ¯ мон) – (пр ¯ шок)) £ 1). Тогда

(мон®шок ®Х) уд (пр £ <мон, шок> OR (пр ³ <мон, шок> AND (0 £ ((прмон) – (пршок)) £ 1))) Þ

Þ (0 £ ((пр ¯ мон) – (пр ¯ шок))£1),

так как <> ¯ мон = <> ¯ шок = <мон> ¯ шок = 0, <мон> ¯ мон = <мон, шок> ¯ мон = <мон, шок> ¯ шок = 1 и пр ³ <мон ,шок> Þ (пр ¯ мон = пр" ¯ мон + 1 AND пр ¯ шок = пр" ¯ шок+1)

Применяя теперь закон L3, а затем — L6, получим требуемый результат.

Тот факт, что процесс Р удовлетворяет спецификации, еще не означает, что он будет нормально функционировать. Например, так как

пр = <> Þ 0 £ ((пр ¯ мон) – (пр ¯ шок)) £ 1

то с помощью законов L3, L4 можно доказать, что

СТОП уд0 £ ((пр ¯ мон) – (пр ¯ шок)) £ 1.

Однако СТОП не соответствует ни требованиям владельца торгового автомата, ни покупателя. Он не сделает ничего плохого, но только потому, что он не делает ничего вообще. По той же причине СТОП удовлетворяет любой спецификации, которой может удовлетворять процесс.

– Конец работы –

Эта тема принадлежит разделу:

Математические основы программирования. Теория схем программ. Семантическая теория программ

Следуя А П Ершову мы употребляем термин теоретическое программирование в качестве названия математической дисциплины изучающей синтаксические.. В настоящее время сложились следующие основные направления исследований.. Математические основы программирования Основная цель исследований развитие математического аппарата..

Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Взаимодействующие последовательные процессы

Что будем делать с полученным материалом:

Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:

Все темы данного раздела:

Программа как формализованное описание процесса обработки данных
Целью программирования является описание процессов обработки данных (в дальнейшем - просто процессов). Данные - это представление фактов и идей в формализованном виде, пригодном для п

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

Стандартные схемы программ
1.2.1. Базис класса стандартных схем программ Стандартные схемы программ (ССП) характеризуются базисом и структурой схемы. Базис класса фиксирует символы, из которых строятся схем

Свойства и виды стандартных схем программ
1.3.1. Эквивалентность, тотальность, пустота, свобода ССП S в базисе В тотальна (пуста), если для любой интерпретации I базиса В программа (S, I) останавливается (зацикливает

Моделирование стандартных схем программ
1.4.1. Одноленточные автоматы Конечный одноленточный (детерминированный, односторонний) автомат обнаруживают ряд полезных качеств, используемых в теории схем программ для установлен

Рекурсивные схемы
1.5.1. Рекурсивное программирование Среди упомянутых выше методов формализации понятия вычислимой функции метод Тьюринга — Поста основан на уточнении понятия процесса вычислений, для чего

Трансляция схем программ
1.6.1. О сравнении класс сов схем. Программы для ЭВМ, будь-то программы, записанные на операторном языке, или программы на рекурсивном языке, универсальны в том смысле, что любую вычислиму

Обогащенные и структурированные схемы
1.7.1 Классы обогащенных схем Выделяют следующие классы обогащенных схем: класс счетчиковых схем, класс магазинных схем, класс схем с массивами. Классы счетчиковых и магази

Описание смысла программ
Существует несколько причин, по которым следует заниматься описанием семантикипрограмм, или смысла выражений, операторов и программных единиц. Руководство по использованию языка про

Преобразователь предикатов.
Э. Дейкстра рассматривает слабейшие предусловия, т.е. предусловия, необходимые и достаточные для гарантии желаемого результата. «Условие, характеризующее множество всех начальных состояний

Языки формальной спецификации.
Языки и методы формальной спецификации, как средство проектирования и анализа программного обеспечения появились более сорока лет назад. За это время было немало попыток разработать как универсальн

Методы доказательства правильности программ.
Как известно, универсальные вычислительные машины могут быть запрограммированы для решения самых разнородных задач - в этом заключается одна из основных их особенностей, имеющая огромную практическ

Правила верификации К. Хоара.
Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желае

Параллельные процессы
Процесс определяется полным описанием его потенциального поведения. При этом часто имеется выбор между несколькими различными действиями. В каждом таком случае выбор того, какое из событий произойд

Программирование параллельных вычислений
3.5.1. Основные понятия Исполнение процессов типичной параллельной программы прерывается значительно чаще, чем процессов, работающих в последовательной среде, так как процессы параллельной

Модели параллельных вычислений
Параллельное программирование представляет дополнительные источники сложности - необходимо явно управлять работой тысяч процессоров, координировать миллионы межпроцессорных взаимодействий. Для того

Основные определения
4.2.1. Теоретико-множественное определение сетей Петри Пусть мультимножество это множество, допускающее вхождение нескольких экземпляров одного и того же элемента. Сеть

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

Then begin
X1:=X1*Y; end; X2:=X2*Y; Y:=Y-1; end; write(X1); write(X2); endРисунок 4.5.

Анализ сетей Петри
Моделирование систем сетями Петри, прежде всего, обусловлено необходимостью проведения глубокого исследования их поведения. Для проведения такого исследования необходимы методы анализа свойств сами

Хотите получать на электронную почту самые свежие новости?
Education Insider Sample
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
Реклама
Соответствующий теме материал
  • Похожее
  • Популярное
  • Облако тегов
  • Здесь
  • Временно
  • Пусто
Теги