ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ. Теория вычислительных процессов

• Название: Теория вычислительных процессов
• Анкор: ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ.doc
• Дата: 01.04.2018
• Размер: 2.17 Mb.
• Имя файла: ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ.doc
• Тип: Документы; #17485
• страница: 13 из 20

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

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

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

Пример 3.12. протоколы(ЧАСЫ) = {<>, <тик>,<тик, тик>,…} = {тик}^*. Здесь множество протоколов бесконечно.

Законы

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

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

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

L2. протоколы(с Р) = {t t= <> OR (t₀ = cANDt' протоколы(Р))}

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

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

L3.протоколы(x: B Р(x)) =

={t t= <> OR (t₀ ВANDt' протоколы(Р(t₀)))}.

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

L4.протоколы(Х: А.F(Х)) = _n0 протоколы(Fⁿ(СТОП_A)).

Пример3.13. протоколы(ТАП) = _n0 {s  s <мон, шок>ⁿ}.

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

1) Согласно предположению индукции

протоколы(Fⁿ(ТAП)) = {t  t <мон, шок>ⁿ},

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

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

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

протоколы(Fⁿ⁺¹(СТОП)) = протоколы(мон шок Fⁿ(СТОП)) =

= {<>, <мон>} {<мон, шок>^tt протоколы(Fⁿ(СТОП))} =

= {<>, {<мон>} {<мон, шок>^t  t <мон, шок>ⁿ} =

= {s  s= <> OR s= <мон> OR t.s =<мон, шок>^t AND t <мон, шок>ⁿ}

= {s  s <мон, шок>ⁿ⁺¹}.

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

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

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

L7.протоколы(P) {P}^*.

После

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

Пример 3.14. (ТАП / <мон>) = (шок → ТАП).
Спецификации
Спецификация изделия – это описание его предполагаемого поведения. Это описание представляет собой предикат, содержащий свободные переменные, каждая из которых соответствует некоторому обозримому аспекту поведения изделия.

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

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

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

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

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

НЕУБЫТ= (#(пр{шок}) #(пр{мон})) = пр шок пр мон.

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

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

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

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

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

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

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

пр.пр препротоколы(Р) S.

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

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

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

L2А.Если Р уд S и Р уд Т, то Р уд (SAND 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 (пр₀ = cAND S(пр'))).

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

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

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

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

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

(Х.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.

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