методичка (811291), страница 9

Файл №811291 методичка (Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL) 9 страницаметодичка (811291) страница 92020-08-21СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 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’

Упражнения

  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одержит перечисление имен каналов с указанием типа передаваемых посредством них значений и имеет вид:

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, этот же тип имеет и всё выражение. Отличие взаимной блокировки от параллельной композиции (||) состоит в том, что в течение параллельного вычисления не происходит взаимодействия с окружением, оно становится возможным только после снятия взаимной блокировки в результате завершения вычисления одного из выражений. Таким образом, взаимная блокировка вынуждает выражения взаимодействовать друг с другом.

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

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

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

Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6508
Авторов
на СтудИзбе
302
Средний доход
с одного платного файла
Обучение Подробнее