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

Текст из файла (страница 9)

variable id : t := value_expr

in

value_expr₁ ; ... ; value_expr_n

end, где n  1.

Такая конструкция задает блок, внутри которого описывается локальная переменная id типа t с начальным значением, определяемым выражением value_expr (указывать начальное значение необязательно). Областью видимости локальной переменной является блок, в котором она описана.

Аналогичным образом можно локально описывать типы, функции и аксиомы.

Явные и неявные спецификации в императивном стиле

В качестве примера явной спецификации в императивном стиле приведем спецификацию функции increase, увеличивающей на 1 значение счетчика, представленного переменной counter.

variable counter : Nat := 0

value

increase : Unit -> write counter Nat

increase() is

counter := counter + 1; counter

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

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

variable set1 : Int-set

value

choose : Unit -~-> write set1 Int

choose() as res

post res isin set1’ /\ set1 = set1’ \ {res}

pre set1 ~= { }

Первая часть постусловия (res isin set1’) выражает тот факт, что до вызова функции элемент присутствовал в множестве, вторая (set1 = set1’ \ {res}) гласит, что новое значение переменной set1 должно совпадать с ее значением до вызова функции за исключением удаляемого элемента.

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

x = x’

Упражнения

1. Упростить выражения:

1. x := 1; x := 2

2. (x :=1; x) + (x := 2; x)

3. (x :=2; x) + (x := 1; x)

1. Построить моделе-ориентированную спецификацию стека в императивном стиле. Спецификация должна описывать следующие функции:

• пустой стек,

• поместить элемент в стек,

• удалить верхний элемент непустого стека,

• проверить стек на пустоту,

• найти значение верхнего элемента непустого стека (без удаления из стека).

1. Использовать явное описание функций.

2. Использовать неявное описание функций.

Указания:

• для представления стека используйте переменную списочного типа,

• в сигнатуре функций опишите соответствующие права доступа к этой переменной.

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

1. конструкцию цикла while,

2. конструкцию цикла until,

3. конструкцию цикла for.

1. По явной спецификации функции построить ее неявную спецификацию:

1. value

f : Int >< Int >< Int -> write x, y Int >< Int

f(a,b,c) is

if a = b then

(if a + b > с then с else x := y; a + b end,

b * (if с > 0 then x :=c; с else 0 – с end))

else (y :=a + b; y,a - b) end

1. variable v1, v2 : Int

value

f : Int >< Bool > -> write v1read v2 Nat >< Bool

f(a,b) is

local variable n : Int in

if b then v1 := v2 * a; n := v1 ** 2 + v2 ** 2

else n := if v1 > v2 then v1 ** 2 – v2 ** 2

else v2 ** 2 – v1 ** 2 end

end;

if v1 > v2 tnen v1 := v2 end;

(n, v1 = v2)

end

ГЛАВА 9. СПЕЦИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ ПРОЦЕССОВ

Каналы и взаимодействие процессов. Функции с доступом к каналам. Выражения взаимодействия. Композиция параллельных выражений: параллельная композиция, внутренний выбор, внешний выбор, взаимная блокировка. Упрощение параллельных выражений. Упражнения.

Каналы и взаимодействие процессов

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

Объявление каналов производится в разделе channel. Каждое отдельное описание этого раздела cодержит перечисление имен каналов с указанием типа передаваемых посредством них значений и имеет вид:

id₁, … ,id_n : type_expr, где n  1.

Например:

channel a : Nat,

c, b : Int

Функции с доступом к каналам

Функции, имеющие доступ к каналам, в RSL называются также процессами. В сигнатуре таких функций доступ к каналам описывается в форме:

in id₁, ..., id_n, n  1,

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

out id₁, ..., id_n, n  1,

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

В качестве примера рассмотрим следующий фрагмент спецификации:

channel a ,b: Nat

value p : Unit -> in a out b Unit

Здесь функция p может вводить значения типа Nat по каналу a и выводить значения того же типа по каналу b.

Выражения взаимодействия

В RSL предусмотрено два примитива взаимодействия: один для ввода значения из канала, другой для вывода значения в канал. Если имеется следующее объявление канала:

channel id: T

то ввод значения из этого канала специфицируется выражением ввода вида:

id?

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

Например, выражение:

a := c?

специфицирует факт присваивания переменной a значения, введенного по каналу c.

Вывод значения в канал специфицируется выражением вывода вида:

id! value_expr

Вычисление такого выражения начинается с вычисления выражения value_expr, значение которого выводится в канал id. На этом вычисление выражения вывода приостанавливается до тех пор, пока выведенное значение не будет потреблено из канала каким-либо другим процессом. Таким образом, для завершения вычисления выражения вывода также должно произойти взаимодействие процессов посредством указанного в выражении канала. Тип выражения value_expr должен совпадать с типом канала id. Типом выражения вывода является тип Unit.

В качестве примера рассмотрим спецификацию процесса opb, моделирующего одноместный буфер, взаимодействующий с окружением посредством каналов add и get. Значения типа Elem вводятся из канала add и затем выводятся в канал get.

scheme ONE_PLACE_BUFFER =

class

type Elem

channel add, get : Elem

value opb : Unit -> in add out get Unit

axiom opb() is let v = add? in get!v end; opb()

end

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

Композиция параллельных выражений

В RSL предусмотрено четыре вида композиции параллельных выражений:

• параллельная композиция,

• внешний выбор,

• внутренний выбор,

• взаимная блокировка (interlock).

Параллельная композиция

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

value_expr₁ || value_expr₂

Указанные выражения вычисляются параллельно до тех пор, пока одно из них не завершится, в то время как другое продолжит свое вычисление. Оба выражения должны иметь тип Unit, этот же тип имеет и всё выражение. Символ || обозначает комбинатор параллельной композиции.

Например, пусть имеются следующие объявления:

channel c : Int

variable x : Int

Тогда параллельная композиция выражений x := c? и c!5 задается выражением:

x := c? || c!5

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

x := 5

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

(x := c? || c!5) || c!7

может привести к одному из следующих эффектов:

• x := 7; c!5

• x := 5; c!7

• взаимодействие не происходит

Комбинатор параллельной композиции обладает свойствами коммутативности и ассоциативности.

Внешний выбор

Внешний выбор задается выражением вида:

value_expr₁ |=| value_expr₂

Выражения value_expr₁ и value_expr₂ должны иметь одинаковый тип, который считается также и типом всего выражения внешнего выбора. В результате внешнего выбора из двух указанных выражений для вычисления выбирается только одно, причем на выбор может оказать влияние окружение, т.е. другие выражения, вычисляющиеся параллельно с данным. Именно поэтому в названии данной композиции фигурирует термин «внешний». Символ |=| обозначает комбинатор внешнего выбора.

Внешний выбор служит для спецификации выбора между различными видами взаимодействия. Например, в области видимости объявлений:

channel c , d: Int

variable x : Int

рассмотрим выражение внешнего выбора:

x := c? |=| d!5

Это выражение предлагает два вида взаимодействия: ввод из канала c или вывод в канал d. Предположим, данное выражение вычисляется в следующем окружении:

(x := c? |=| d!5) || c!1

Тогда возможный эффект вычисления такого выражения состоит в выполнении взаимодействия посредством канала c, в результате чего получается выражение:

x := 1

В данном случае выбор в пользу первого выражения диктуется окружением (c!1).

Комбинатор внешнего выбора обладает свойствами коммутативности и ассоциативности.

Внутренний выбор

Внутренний (недетерминированный) выбор задается выражением вида:

value_expr₁ |^| value_expr₂ ,

где выражения value_expr₁ и value_expr₂ должны иметь одинаковый тип, который совпадает с типом всего выражения. В результате внутреннего выбора из двух выражений для вычисления выбирается только одно, причем в отличие от предыдущего случая окружение не оказывает никакого влияния на этот выбор. Символ |^| обозначает комбинатор внутреннего выбора.

Например, в выражении:

(x := c? |^| d!5) || c!1

выражение c!1 не влияет на то, какое из выражений x := c? или d!5 выбирается. Если внутренний выбор выпадает на x:=c?, то результатом является выражение:

x:= c? || c!1,

потенциально приводящее к взаимодействию через канал c. Если выбор выпадает на d!5, то результатом оказывается выражение:

d!5 || c!1,

препятствующее внутренним взаимодействиям.

Комбинатор внутреннего выбора также обладает свойствами коммутативности и ассоциативности.

Взаимная блокировка (interlock)

Взаимная блокировка (interlock) задается выражением вида:

value_expr₁ ++ value_expr₂ ,

где ++ обозначает комбинатор взаимной блокировки. Указанные выражения вычисляются параллельно, блокируя друг друга по отношению к внешним взаимодействиям, до тех пор, пока одно из них не завершится, в то время как другое продолжит свое вычисление. Оба выражения должны иметь тип Unit, этот же тип имеет и всё выражение. Отличие взаимной блокировки от параллельной композиции (||) состоит в том, что в течение параллельного вычисления не происходит взаимодействия с окружением, оно становится возможным только после снятия взаимной блокировки в результате завершения вычисления одного из выражений. Таким образом, взаимная блокировка вынуждает выражения взаимодействовать друг с другом.

Комбинатор взаимной блокировки обладает свойством коммутативности, но не является ассоциативным.

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

Список файлов книги