методичка (811291), страница 9
Текст из файла (страница 9)
variable id : t := value_expr
in
value_expr1 ; ... ; value_exprn
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’
Упражнения
-
Упростить выражения:
-
x := 1; x := 2
-
(x :=1; x) + (x := 2; x)
-
(x :=2; x) + (x := 1; x)
-
Построить моделе-ориентированную спецификацию стека в императивном стиле. Спецификация должна описывать следующие функции:
-
пустой стек,
-
поместить элемент в стек,
-
удалить верхний элемент непустого стека,
-
проверить стек на пустоту,
-
найти значение верхнего элемента непустого стека (без удаления из стека).
-
Использовать явное описание функций.
-
Использовать неявное описание функций.
Указания:
-
для представления стека используйте переменную списочного типа,
-
в сигнатуре функций опишите соответствующие права доступа к этой переменной.
-
Построить явную спецификацию в императивном стиле функции fract_sum, вычисляющей частичную сумму натурального ряда, используя:
-
конструкцию цикла while,
-
конструкцию цикла until,
-
конструкцию цикла for.
-
По явной спецификации функции построить ее неявную спецификацию:
-
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
-
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одержит перечисление имен каналов с указанием типа передаваемых посредством них значений и имеет вид:
id1, … ,idn : type_expr, где n 1.
Например:
channel a : Nat,
c, b : Int
Функции с доступом к каналам
Функции, имеющие доступ к каналам, в RSL называются также процессами. В сигнатуре таких функций доступ к каналам описывается в форме:
in id1, ..., idn, n 1,
где перечисляются каналы ввода, из которых функция может получать значения, или в форме:
out id1, ..., idn, 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_expr1 || value_expr2
Указанные выражения вычисляются параллельно до тех пор, пока одно из них не завершится, в то время как другое продолжит свое вычисление. Оба выражения должны иметь тип 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_expr1 |=| value_expr2
Выражения value_expr1 и value_expr2 должны иметь одинаковый тип, который считается также и типом всего выражения внешнего выбора. В результате внешнего выбора из двух указанных выражений для вычисления выбирается только одно, причем на выбор может оказать влияние окружение, т.е. другие выражения, вычисляющиеся параллельно с данным. Именно поэтому в названии данной композиции фигурирует термин «внешний». Символ |=| обозначает комбинатор внешнего выбора.
Внешний выбор служит для спецификации выбора между различными видами взаимодействия. Например, в области видимости объявлений:
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_expr1 |^| value_expr2 ,
где выражения value_expr1 и value_expr2 должны иметь одинаковый тип, который совпадает с типом всего выражения. В результате внутреннего выбора из двух выражений для вычисления выбирается только одно, причем в отличие от предыдущего случая окружение не оказывает никакого влияния на этот выбор. Символ |^| обозначает комбинатор внутреннего выбора.
Например, в выражении:
(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_expr1 ++ value_expr2 ,
где ++ обозначает комбинатор взаимной блокировки. Указанные выражения вычисляются параллельно, блокируя друг друга по отношению к внешним взаимодействиям, до тех пор, пока одно из них не завершится, в то время как другое продолжит свое вычисление. Оба выражения должны иметь тип Unit, этот же тип имеет и всё выражение. Отличие взаимной блокировки от параллельной композиции (||) состоит в том, что в течение параллельного вычисления не происходит взаимодействия с окружением, оно становится возможным только после снятия взаимной блокировки в результате завершения вычисления одного из выражений. Таким образом, взаимная блокировка вынуждает выражения взаимодействовать друг с другом.
Комбинатор взаимной блокировки обладает свойством коммутативности, но не является ассоциативным.