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

Если Р - объект, отвечающий спецификации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, то Р уд Т.

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

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

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

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

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

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

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

L5.Если "x B.(Р(x) уд S(пр, х)), то

(х: В Р(x)) уд (пр = <> OR (пр₀ B AND S(пр', пр₀))).

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

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.

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

Параллельные процессы

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

Взаимодействие

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

Законы

Законы, управляющие поведением (P || Q), параллельно развивающихся процессов P и Q, достаточно просты. Первый закон выражает логическую симметрию между процессом и его окружением:

L1.P || Q = Q || P.

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

L2.P || (Q || R) = (P || Q) || R.

Процесс, находящийся в тупиковой ситуации, приводит к тупику всей системы.

L3.P || СТОП_aP = СТОП_aP.

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

L4А. (с Р) || (с Q) = с (Р || Q).

L4B. (с Р) || (d Q) = СТОП.

Параллелизм

Рассмотрим случай, когда операнды Р и Q оператора || имеют неодинаковые алфавиты aР aQ.

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

Таким образом, множество всех событий, логически возможных для данной системы, есть просто объединение алфавитов составляющих ее процессов a(Р || Q) = aР aQ.

Законы

Формальное описание вышесказанного осуществляется с помощью следующих законов:

Пусть а (aР - aQ), b (aQ - aР) и {c, d} (aР aQ). Следующие законы показывают, каким образом процесс Р один участвует в событии a, Q один участвует в b, а c и d требуют одновременного участия P и Q.

L1А. (с Р) || (с Q)=с (Р || Q).

L1B. (с Р) || (d Q)=СТОП.

L2А. (a Р) || (с Q)=a (Р || (с Q)).

L2B.(с Р) || (b Q)=b ((с Р) || Q)..

L3.(a Р) || (b Q)=.(a (Р || (b Q)) | b ((a Р) || Q)).

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

L3.Пусть Р = (х: А Р(х)), Q = (y: B Q(y)). Тогда

Р || Q = (z: C (Р' || Q')),

где С = (A B) (А - aQ) (B - aP), P' = P(z), если z A, иначе P' = Р, а Q' = Q(z), если z B, иначе Q' = Q.

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

Пример 3.17.

Пусть aР = {a, c}, aQ = {b, c}, P = (a c P), Q = (c b Q). Тогда

Р || Q = (a c P) || (c b Q) = a ((c P) || (c b Q)) по L2A

= a c (P || (b Q)), по L1A (1)

(P || (b Q)) = a ((c P) || (b Q)) | b (P || Q) по L3

= a b ((c P) || Q) | b (P || Q)по L2B

= a b c (P || (b Q)) | b a c (P||(b Q)) по L1A и (1)

= mX.(a b c X | b a c X).

Отсюда следует, что

Р || Q = a c mX.(a b c X | b a c X).по (1)

Реализация

Реализация операции || выводится непосредственно из закона L3. Алфавиты операндов представляются конечными списками символов A и B.

Протоколы

Пусть t — протокол (Р || Q). Тогда все события из t, принадлежащие алфавиту aР, являлись событиями в жизни P, а все события из t, не принадлежащие aР, происходили без участия P. Таким образом, (taР) — это протокол всех событий, в которых участвовал процесс P, и поэтому он является протоколом P. По тем же соображениям (taQ) является протоколом Q. Более того, каждое событие из t должно содержаться либо вaР, либо в aQ. Эти рассуждения позволяют сформулировать закон

L1. протоколы(Р || Q) = {t | (t­aР) протоколы(Р)

AND (t­aQ) протоколы(Q) AND t (aР aQ)^*}.

Не нашли, что искали? Воспользуйтесь поиском по сайту: