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

Построить алгебраическую спецификацию стека со следующими функциями:••••поместить элемент в стек,удалить верхний элемент непустого стека,проверить стек на пустоту,найти значение верхнего элемента непустого стека (без удаления изстека).2. Построить алгебраическую спецификацию очереди со следующими функциями:••••добавить элемент в очередь,удалить элемент из непустой очереди,проверить очередь на пустоту,найти значение первого элемента непустой очереди (без удаления изочереди),• подсчитать количество элементов в очереди.Указания: в упражнениях 1, 2 руководствуйтесь общей схемой построенияалгебраической спецификации.393.

Используя абстракцию списков, уточнить построенную алгебраическуюспецификацию стека в моделе-ориентированную спецификацию. Проверитьсогласованность уточнения.4. Используя абстракцию списков, уточнить построенную алгебраическуюспецификацию очереди в моделе-ориентированную спецификацию.

Проверитьсогласованность уточнения.5. Доказать, что вторая спецификация является (или не является) уточнениемпервой.valuef1 : A >< L -~-> L,f2 : A >< L -~->,f3 : L -> Nataxiomall a : A, b : L :f3(f1(a,b)) is f3(b) + 1pre f3(b) = 1,all a : A, b : L :f3(f2(a,b)) is 1 + f3(b)pre f3(b) = 1,all a : A, b : L :f1(a,b) is f2(a,b)pre f3(b) = 1typeL = A-listvaluef1 : A >< L -~-> Lf1(a,b) is <. a .> ^ tl bpre b ~= <..>,f2 : A >< L -~-> Lf2(a,b) is tl b ^ <. a .>pre b ~= <..>,f3 : L -> Natf3(ls) is len ls40ГЛАВА 7.

ВАРИАНТНЫЕ ОПРЕДЕЛЕНИЯПонятие вариантного определения. Виды вариантных определений. Конструкторы,деструкторы и реконструкторы. Упражнения.Понятие вариантного определенияВариантное определениеконструкцией вида:(определениевариантноготипа)задаетсяtype id = = variant1 | ... | variantn , n ≥ 1и предназначено для удобного и компактного определения абстрактного типа ( id)вместе с набором функций и констант над этим типом. Т.е. вариантноеопределение представляет собой сокращенную форму записи определенияабстрактного типа, определения некоторых функций и аксиом. Средиопределяемых функций могут быть:• конструкторы – для генерации значений данного типа,• деструкторы – для декомпозиции значений данного типа,• реконструкторы – для модификации значений данного типа.Аксиомыопределяютсвойстваконструкторов,деструкторовиреконструкторов. Важной аксиомой среди них является аксиома индукции, котораягласит, что данный абстрактный тип полностью генерируется указаннымиконструкторами, т.е.

любое значение этого типа получается в результате конечногочисла применений конструкторов.Виды вариантных определений. Конструкторы, деструкторы иреконструкторыКонструкторы-константыПростейшим видом вариантного определения является использованиеконструкторов-констант, когда тип определяется путем явного перечисления егозначений. В качестве примера рассмотрим вариантное определение:type Colour = = black | whiteОно представляет собой сокращенную форму записи следующего фрагментаспецификации:type Colour/* объявление абстрактного типа */valueblack : Colour,/* определение констант */white : Colouraxiom[ disjoint ]black ~= white,[ induction ]all p : Colour -> Bool :- (p(black) /\ p(white)) => (all с : Colour :- p(c))Первая аксиома гарантирует различие значений black и white.

Вторая (аксиомаиндукции) позволяет доказать, что в типе Colour нет других значений кроме41указанных двух, т.е. данный тип полностью определяется указаннымиконстантами. С помощью аксиомы индукции можно индуктивно доказыватьсвойства над определяемым типом. В частности, для рассмотренного примера этоозначает, что если справедливость некоторого свойства доказана для значений blackи white, то из этого следует справедливость этого свойства для всех значений типаColour.Конструкторы записейБолее сложным видом вариантного определения является использование вкачестве конструкторов функций для генерации значений определяемого типа конструкторов записей (record constructions).

Такие конструкторы используютсяпри определении структур данных. В частности, эти конструкторы могутиспользоваться для генерации записей, где под записью подразумевается наборименованных полей.В качестве примера рассмотрим вариантное определение:type Collection = = empty | add(Elem, Collection),в котором используется конструктор-константа empty и конструктор записи add.Это определение рекурсивно определяет тип Collection, содержащий два видазначений:1. значение empty,2. значения, построенные с помощью конструктора add.Данное вариантное определение представляет собой сокращение следующегофрагмента спецификации:type Collectionvalueempty : Collection,add : Elem ><Collection -> Collectionaxiom[ disjoint ]all el : Elem, с : Collection :- empty ~= add(el,c),[ induction ]all p : Collection -> Bool :(p(empty) /\ (all el : Elem, с : Collection :- p(c) => p (add(el,c)))) =>(all с : Collection :- p(c))ДеструкторыДеструкторами называются функции, предназначенные для выделениякомпонент из значений вариантного типа, с помощью таких функцийосуществляется декомпозиция значений вариантного типа.В качестве примера рассмотрим вариантное определение:type List = = empty | add(head : Elem, tail : List),где появляются два деструктора head и tail, обеспечивающие возможностьдекомпозиции значений, сгенерированных конструктором add, на «голову» и«хвост».Данное вариантное определение является сокращением следующегофрагмента спецификации:42type Listvalueempty : List,add : Elem >< List -> List,head : List -~-> Elem,tail : List -~-> Listaxiom[ disjoint ]all el : Elem, ls : List :- empty ~= add(el,ls),[ induction ]all p : List -> Bool :(p(empty) /\ (all el : Elem, ls : List :- p(ls) => p (add(el,ls)))) =>(all ls : List :- p(ls))[ head_add ]all el : Elem, ls : List :- head(add(el,ls)) is el,[ tail_add ]all el : Elem, ls : List :- tail(add(el,ls)) is lsСледует обратить внимание на частичность деструкторов head и tail, посколькусогласно исходному вариантному определению они определены только надзначениями, сгенерированными конструктором add.РеконструкторыРеконструкторами называются функции, предназначенные для изменениязначений отдельных компонент значений вариантного типа.

С помощьюреконструкторов осуществляется модификация значений вариантного типа.В качестве примера рассмотрим предыдущее определение типа List сдобавлением реконструктора replace_head для обеспечения возможности измененияголовы списка.type List = = empty | add(head : Elem <-> replace_head, tail : List)Вхождение реконструктора добавит к вышеприведенной спецификацииследующий фрагмент:valuereplace_head : Elem >< List -~-> Listaxiom[ head_ replace_head ]all el,el1 : Elem, ls : List :- head(replace_head(el,add(el1,ls))) is el,/* изменилось значение головы списка */[ tail_ replace_head ]all el : Elem, ls : List :- tail(replace_head(el,ls)) is tail(ls)pre ls ~= empty/* реконструктор replace_head не меняет хвост списка */Первая аксиома выражает эффект изменения значения отдельной компонентыпутем применения соответствующего реконструктора.

Вторая аксиома выражаеттот факт, что изменение реконструктором значения некоторой компоненты неоказывает никакого эффекта на другие компоненты.43Упражнения1. Cчитая определенными абстрактные типы Key и Data, построить вариантноеопределение записи с полями «ключ» и «значение». Привести эквивалентноеопределение без использования вариантных определений.Указания: используйте конструктор записей и деструкторы для декомпозициизаписи на значения ее полей.2.

Cчитая определенным абстрактный тип Elem, построить вариантноеопределение стека. Привести эквивалентное определение без использованиявариантных определений.Указания: воспользуйтесь рекурсивным определением стека.3. Для следующих вариантных определений привести эквивалентные определениябез использования вариантных определений.(a) type Elem,(b)(c)(d)Collection = = empty | add1(Elem, Collection) |add2(Elem, Elem, Collection)type Elem,Tree = = empty | node(left : Tree, val : Elem, rigth : Tree)type Elem,Tree = = empty | node(left : Tree, val : Elem <-> repl_val, rigth : Tree)type Figure = = box(length : Real, width : Real) | circle(radius : Real) |triangle(base_line : Real, left_angle : Real, right_angle : Real)44ГЛАВА 8. ИМПЕРАТИВНЫЙ СТИЛЬ СПЕЦИФИКАЦИЙПонятие императивного стиля спецификаций.

Описание переменных. Выражениеприсваивания. Функции с доступом к переменным. Императивные конструкцииRSL. Описание локальных переменных. Явные и неявные спецификации вимперативном стиле. Упражнения.Понятие императивного стиля спецификацийСпецификации в языке RSL могут разрабатываться как в аппликативном, так ив императивном стиле. Аппликативный стиль ближе к функциональному стилюпрограммирования, именно этот стиль был использован во всех рассмотренныхранее спецификациях.