Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 9

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

В RSL переменная рассматривается как контейнер,способный хранить значения определенного типа. Значение переменной можетбыть изменено путем присваивания ей нового значения. Совокупность значенийвсех объявленных в данной спецификации переменных формирует понятиесостояния спецификации.Описание переменныхОписание переменных в языке RSL производится в разделе variable, при этомкаждое отдельное описание переменной имеет вид:id : type_expr := value_expr,где id задает имя переменной, type_expr – ее тип, выражение value_expr определяетначальное значение переменной.

Инициализация переменной ее начальнымзначением является необязательной, и если она не указана, начальным значениемпеременной считается произвольное значение данного типа. Однотипныепеременные без начального значения могут объявляться в одном описании.Например:variable n : Nat := 1,s : Real = 0.0,a, b : IntОбластью видимости переменной считается весь модуль, в котором даннаяпеременная описана.45Выражение присваиванияДля изменения значения переменной в RSL используется выражениеприсваивания вида:id := value_exprВ качестве побочного эффекта при вычислении такого выражения переменнойid присваивается значение выражения value_expr, при этом само выражениеприсваивания возвращает значение () типа Unit.

Типы переменной id и выраженияvalue_expr должны быть согласованы, причем тип выражения value_expr не можетбыть типом Unit. Пример выражения присваивания:counter := counter +1Функции с доступом к переменнымВ сигнатуре функций, имеющих доступ к переменным, обязательно должноуказываться описание доступа к этим переменным в форме:write id1, ..., idn, n ≥ 1,если функция имеет доступ к перечисленным переменным на запись (и чтение),или в форме:read id1, ..., idn, n ≥ 1,если указанные переменные доступны только на чтение. Если функция имеетдоступ к переменным на запись, то в качестве своего побочного эффекта она можетизменять значения данных переменных.В качестве примера рассмотрим следующий фрагмент спецификации:variable n, m : Natvaluef1 : Unit -> write n Nat,f2 : Unit -> read m Nat,f3 : Nat -> write n read m NatЗдесь функции f1 и f2 не имеют входных параметров и, следовательно, зависяттолько от конкретного состояния, в котором происходит их вычисление.

При этомf1 имеет доступ к переменной n на чтение и запись, f2 – к переменной m только начтение. Функция f3 имеет доступ к переменной n на чтение и запись и кпеременной m только на чтение.Императивные конструкции RSLПоследовательность выраженийПоследовательная композиция двух выражений задается выражением вида:value_expr1 ; value_expr2Вычисление такого выражения начинается с вычисления выражения value_expr1 сцелью достижения его возможного побочного эффекта в виде изменения значений46входящих в него переменных.

Затем уже в измененном состоянии вычисляетсявыражение value_expr2. В качестве результата вычисления последовательнойкомпозиции выражений возвращается значение выражения value_expr2. Выражениеvalue_expr1 должно иметь тип Unit. Например:x := 1; xx := x + 1; x- выражение возвращает значение 1,- выражение возвращает увеличенное на 1 значение переменной x.В общем случае произвольная последовательность выражений задаетсявыражением:value_expr1 ; ... ; value_exprn , где n > 1.При вычислении такого выражения последовательно слева направо вычисляютсявсе входящие в него выражения, в качестве результата вычисления возвращаетсязначение выражения value_exprn.

Все выражения кроме последнего должны иметьтип Unit.Выражение ifВыражение if в императивных спецификациях имеет традиционную форму:if value_expr then value_expr1 else value_expr2 end,спецификой является только то, что выражения value_expr1 и value_expr2 имеют типUnit. Кроме того возможна сокращенная форма выражения в виде:if value_expr then value_expr1 endЭта форма эквивалентна выражению:if value_expr then value_expr1 else skip end,где skip представляет предопределенное выражение типа Unit, не имеющеепобочного эффекта.Например:if counter > 0 then counter := counter - 1 endКонструкции цикловВ императивных спецификациях RSL используются три конструкции цикловдля повторяющегося вычисления выражений, указанных в теле цикла:• цикл с предусловием (while),• цикл с постусловием (until),• цикл с заранее известным числом повторений ( for).Выражение, задающее любую конструкцию цикла, имеет тип Unit,назначением такого выражения является повторяющееся вычисление указанных втеле цикла выражений с целью достижения их побочного эффекта, выражающегосяв изменении значений переменных.

Семантика конструкций цикла аналогичнасемантике соответствующих конструкций в языках программирования.Цикл whileКонструкция цикла while представлена выражением while вида:47while value_expr do value_expr1 end,где выражение value_expr (тип Bool) задает условие повторения цикла, выражениеvalue_expr1 (тип Unit) – тело цикла (обычно последовательность выражений).Вычисление выражения while состоит из выполнения последовательных итераций.Каждая итерация цикла начинается с вычисления условия value_expr, и в случае егоистинности выполняется вычисление выражения value_expr1, после чего итерацияповторяется, в противном случае вычисление выражения while завершается.Цикл untilКонструкция цикла until представлена выражением until вида:do value_expr1 until value_expr endНазначение выражений value_expr и value_expr1 аналогично их назначению впредыдущей конструкции с той лишь разницей, что value_expr обозначает условиезавершения цикла и в случае истинности этого условия вычисление выраженияuntil завершается.Цикл forКонструкция цикла for представлена выражением for вида:for list_limitation do value_expr1 end,где list_limitation задает список (возможно пустой) значений переменной цикла.

Телоцикла (выражение value_expr1) последовательно вычисляется для всех значений изуказанного списка. Например:for i in <. 1 .. n .> doresult := result + 1.0 / (real i)endОписание локальных переменныхВ императивных спецификациях часто бывает удобно использовать локальныепеременные. Объявление локальной переменной имеет вид:localvariable id : t := value_exprinvalue_expr1 ; ... ; value_exprnend, где n ≥ 1.Такая конструкция задает блок, внутри которого описывается локальнаяпеременная id типа t с начальным значением, определяемым выражением value_expr(указывать начальное значение необязательно).

Областью видимости локальнойпеременной является блок, в котором она описана.Аналогичным образом можно локально описывать типы, функции и аксиомы.48Явные и неявные спецификации в императивном стилеВ качестве примера явной спецификации в императивном стиле приведемспецификацию функции increase, увеличивающей на 1 значение счетчика,представленного переменной counter.variable counter : Nat := 0valueincrease : Unit -> write counter Natincrease() iscounter := counter + 1; counterПри составлении неявных спецификаций в императивном стиле возникаетследующая проблема: если функция имеет побочный эффект, то приспецифицировании результата ее выполнения необходимо уметь различатьзначения соответствующих переменных в состоянии до вызова функции и посленего.

Для этого в RSL предусмотрено выражение id’, которое обозначает значениепеременной id в состоянии до вызова функции.Как пример такой спецификации рассмотрим неявную спецификациюфункции choose, возвращающей в качестве результата произвольный элементмножества с одновременным удалением этого элемента из множества:variable set1 : Int-setvaluechoose : Unit -~-> write set1 Intchoose() as respost res isin set1’ /\ set1 = set1’ \ {res}pre set1 ~= { }Первая часть постусловия (res isin set1’) выражает тот факт, что до вызовафункции элемент присутствовал в множестве, вторая ( set1 = set1’ \ {res}) гласит, чтоновое значение переменной set1 должно совпадать с ее значением до вызовафункции за исключением удаляемого элемента.Итак, при разработке неявных спецификаций в императивном стиленеобходимо учитывать следующую рекомендацию.

В спецификациях функций спобочным эффектом, имеющих доступ к переменным по записи, необходимо впостусловии специфицировать эффект изменения этих переменных. В частности,если изменения значения переменной не происходит, специфицировать этот фактвыражением вида:x = x’Упражнения1.Упростить выражения:(a) x := 1; x := 2(b) (x :=1; x) + (x := 2; x)(c) (x :=2; x) + (x := 1; x)492. Построить моделе-ориентированную спецификацию стека в императивномстиле. Спецификация должна описывать следующие функции:•••••(a)(b)пустой стек,поместить элемент в стек,удалить верхний элемент непустого стека,проверить стек на пустоту,найти значение верхнего элемента непустого стека (без удаления изстека).Использовать явное описание функций.Использовать неявное описание функций.Указания:• для представления стека используйте переменную списочного типа,• в сигнатуре функций опишите соответствующие права доступа к этойпеременной.3.

Построить явную спецификацию в императивном стиле функции fract_sum,вычисляющей частичную сумму натурального ряда, используя:(a)(b)(c)конструкцию цикла while,конструкцию цикла until,конструкцию цикла for.4. По явной спецификации функции построить ее неявную спецификацию:(a)(b)valuef : Int >< Int >< Int -> write x, y Int >< Intf(a,b,c) isif 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) endvariable v1, v2 : Intvaluef : Int >< Bool > -> write v1read v2 Nat >< Boolf(a,b) islocal variable n : Int inif b then v1 := v2 * a; n := v1 ** 2 + v2 ** 2else n := if v1 > v2 then v1 ** 2 – v2 ** 2else v2 ** 2 – v1 ** 2 endend;if v1 > v2 tnen v1 := v2 end;(n, v1 = v2)end50ГЛАВА 9.

СПЕЦИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ ПРОЦЕССОВКаналы и взаимодействие процессов. Функции с доступом к каналам. Выражениявзаимодействия. Композиция параллельных выражений: параллельная композиция,внутренний выбор, внешний выбор, взаимная блокировка. Упрощениепараллельных выражений. Упражнения.Каналы и взаимодействие процессовRSL предоставляет возможность специфицировать параллельные процессы засчет имеющихся в языке средств для спецификации параллельного вычислениявыражений. При этом вычисляющиеся параллельно выражения могутвзаимодействовать между собой посредством каналов, что обеспечиваетсяналичием в языке соответствующих примитивов взаимодействия.Объявление каналов производится в разделе channel.