Законы.

1. Два процесса, определённые с помощью оператора выбора различны, если на первом шаге они предлагают разл. альтернативы или после одинакового первого шага ведут себя по-разному.
2. Всякое должным образом предварённое рекурсивное уравнение имеет единственное решение.

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

Описание процесса, начинающегося с префикса, называют предваренным.

Примеры:

<x,y>, <x>, < >.

Представление асинхронных процессов в метамодели Хоара.

Алфавит – множество имен событий, выбранных для конкретного описания объекта.

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

Процесс (по Красюку) – это кортеж действий.

Протокол (по Красюку) есть процесс.

Если Красюку этого будет мало или если он скажет, что это неправильно, то толкаем следующее ниже.

В метамодели Хоара процесс представляет собой кортеж действий.

Префиксы. Пусть х – событие, а Р – процесс. Тогда запись ( х -> Р ) обозначает объект, который сначала участвует в событии х, а затем ведёт себя точно как Р. Процесс ( x -> P ) имеет по определению тот же алфавит, что и Р.

Рекурсия. Описывается с помощью «префиксной» записи: Р = ( х -> Р ).

Выбор. ( x -> P | y -> Q ). Порядок записи не важен!

Законы.

1. Два процесса, определённые с помощью оператора выбора различны, если на первом шаге они предлагают разл. альтернативы или после одинакового первого шага ведут себя по-разному.
2. Всякое должным образом предварённое рекурсивное уравнение имеет единственное решение.

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

Описание процесса, начинающегося с префикса, называют предваренным.

Примеры:

<x,y>, <x>, < >.

Операции над процессами в метамодели Хоара.

Процесс – кортеж действий.

Протокол – процесс.

//s, t, u – протоколы.

//S, T, U – множества протоколов.

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

Строит новый протокол из пары операндов s и t, просто соединяя их в указанном порядке, результат – s ^ t.

Пример: <n1> ^ <n1> = <n1, n1>

Свойства конкатенации: она ассоциативна; пустой протокол < > служит для нее единицей.