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

Областью определения (доменом) для первогоотображения является множество {3,5}, областью его значений – множество {true,false}, для второго отображения такими множествами являются  {″Klaus″,″John″,″Mary″} и {2,7}.Каждая пара отображения задается выражением v +> w и определяетотображение ключа v в значение w.

Порядок следования пар в отображениинесущественен,поэтому,например,выражения[3 +> true,5 +> false]и[5 +> false,3 +> true] определяют одно и то же отображение.Тип отображения задается типовым выражением:T1 –m-> T2,где T1 - тип элементов домена отображения (ключей) и T2 – тип элементов областизначений отображения. Так, приведенные выше отображения имеют типы  Nat -m->Bool и Text -m-> Nat соответственно.Отображение может быть конечным или бесконечным в зависимости от того,конечным или бесконечным является набор пар, определяющий это отображение.Конечное отображение имеет вид:[v1 +> w1,…,vn +> wn],бесконечное отображение имеет вид:[v1 +> w1,…,vn +> wn,…],где n ≥ 0, vi и wi – некоторые выражения типа T1 и T2 соответственно.Отображение может быть детерминированным или недетерминированным приприменении к элементам из его домена.

Для детерминированного отображениясправедливо свойство уникальности ключа, т.е. верно соотношение:30vi = vk => wi = wk ,где vi и vk – любые элементы из домена этого отображения.Примером конечного детерминированного отображения может служить любоеиз приведенных выше отображений. В качестве примера конечногонедетерминированного отображения можно привести отображение:[3 +> true,3 +> false].Способы определения отображенийДля определения отображений в RSL используются те же способы, что и длямножеств и списков, а именно: непосредственное перечисление элементов исокращенное выражение.

Первый способ может применяться для конечныхотображений, в этом случае отображение задается выражением вида:[v1 +> w1,…,vn +> wn],где n ≥ 0 (в частности, при n = 0 имеем пустое отображение []). Здесьвыражения vi задают значения ключей и wi – сопоставляемых им значений. Именноэтот способ был использован во всех рассмотренных ранее примерах.Сокращенное выражение (comprehended map expression) используется дляопределения значений как конечных, так и бесконечных отображений и имеет вид:[ value_expr_pair | set_limitation ],где выражение value_expr_pair задает общую формулу для определения входящих вотображение пар, set_limitation задает возможные ограничения на доменотображения. Например, значением сокращенного выражения:[ n +> 2∗n | n : Nat :- n <= 2 ]является конечное отображение [0 +> 0,1 +> 2,2 +> 4].Выражение:[ n +> 2∗n | n : Nat ] определяет бесконечное отображение [0 +> 0,1 +> 2,2 +> 4,…].Значение отображения для какого-либо конкретного элемента из его домена(применениеотображения)задаетсяспомощьювыражения value_expr1(value_expr2),  где  value_expr1 является выражением, определяющимданное отображение, value_expr2 – выражение для вычисления значениянекоторого элемента из домена отображения.

Например:[″Klaus″ +> 7, ″John″ +> 2, ″Mary″ +> 7](″John″) = 2,[1 +> [″Per″ +> 5, ″Jan″ +> 7], 2 +> [ ]](1)(″Jan″) == [″Per″ +> 5, ″Jan″ +> 7] (″Jan″) = 7,или для недетерминированного отображения:[3 +> true,3 +> false](3) = true |^| false,31где символ |^| означает недетерминированный (внутренний) выбор из двухуказанных значений. Для значений, не принадлежащих домену отображения,эффект применения отображения не определен, т.е.

соответствующее выражениевозвращает chaos:[1 +> 2, 2 +> 3](5) = chaosОперации над отображениямиНад отображениями определены следующие операции:dom : (T1 –m-> T2) -> T1-infsetrng : (T1 –m-> T2) -> T2-infset!! : (T1 –m-> T2) >< (T1 –m-> T2) -> (T1 –m-> T2)union : (T1 –m-> T2) >< (T1 –m-> T2) -> (T1 –m-> T2)\ : (T1 –m-> T2) >< T1-infset -> (T1 –m-> T2)/ : (T1 –m-> T2) >< T1-infset -> (T1 –m-> T2)# : (T2 –m-> T3) >< (T1 –m-> T2) -> (T1 –m-> T3)Кроме того для отображений определены операции = и ~=.Операции dom и rng возвращают в качестве результата соответственнодомен и область значений отображения, причем в зависимости от видаотображения эти множества могут быть конечными или бесконечными.

Длялюбого отображения m верно соотношение:rng m is {m(x) | x : T1 :- x isin dom m}Примеры:dom [3 +> true, 5 +> false] = {3, 5}rng [3 +> true, 5 +> false] = {true, false}dom [ ] = { }rng [ ] = { }dom [ n +> 2∗n | n : Nat ] = { n | n : Nat }rng [ n +> 2∗n | n : Nat ] = { 2*n | n : Nat }Результатом операции !! (переопределение отображения) является наборпар, полученный объединением наборов пар первого и второго отображений,причем в случае пересечения доменов предпочтение отдается парам из второгоотображения, т.е.

для элементов, попавших в пересечение доменов отображений,второе отображение переопределяет первое. Определение этой операции имеетвид:x !! y is [v +> w | v : T1, w : T2 :- w = y(v) \/ v ~isin dom y /\ w = x(v)]Эффект выполнения данной операции иллюстрируют следующие примеры:[3 +> true, 5 +> false] !! [5 +> true] = [3 +> true, 5 +> true][3 +> true] !! [5 +> false] = [3 +> true, 5 +> false][3 +> true] !! [ ] = [3 +> true]Операция union простоотображений, например:объединяетнаборыпардвухзаданных32[3 +> true, 5 +> false] union [5 +> true] = [3 +> true, 5 +> false, 5 +> true]Эта операция может привести к недетерминизму (как в рассмотренном вышепримере), поэтому во избежание возникновения недетерминизма обычноприменяется к отображениям с непересекающимися доменами.Операции ограничения отображений \ и / позволяют изменять доменыотображений, а именно: \ удаляет из домена отображения указанноемножество, / , напротив, оставляет в домене только те элементы, которыевходят в указанное множество.

Более точно определение этих операций выглядитследующим образом:m \ s = [v +> m(v) | v : T1 :- v isin (dom m) \ s]m / s = [v +> m(v) | v : T1 :- v isin (dom m) inter s]Некоторые примеры:[3 +> true, 5 +> false] \ {5, 7} = [3 +> true][3 +> true, 5 +> false] / {5, 7} = [5 +> false][3 +> true, 5 +> false] \ {3, 5, 7} = [][3 +> true, 5 +> false] / {3, 5, 7} = [3 +> true, 5 +> false]Операция # позволяет осуществлять композицию двух отображений, т.е.для отображений m1 и m2 она определяется так:m1 # m2 = [v +> m1(m2(v)) | v : T1 :- v isin dom m2 /\ m2(v) isin dom m1]Например:[3 +> true, 5 +> false] # [″Klaus″ +> 3, ″John″ +> 7] = [″Klaus″ +> true][3 +> true] # [″Klaus″ +> 5] = [ ]Упражнения1.

Определить отображение, сопоставляющее:(a) каждому нечетному натуральному числу, не превосходящему 30, егоостаток от деления на 3,(b) каждой паре натуральных чисел остаток от деления первого числа на второе(первое число должно быть меньше 50),(c) каждому натуральному числу, не превосходящему 20, все его делители,(d) каждому натуральному числу ближайшее, не превосходящее его, число,являющееся полным квадратом,(e) каждому натуральному числу n, не превосходящему 30, все простые числа издиапазона [2, n]; применить построенное отображение к n = 1, 10, 50.Указания: используйте сокращенное выражение для определения отображений.2. Пример использования абстракции отображений в моделе-ориентированнойспецификации.

Пусть база данных университета описана следующим образом:33schemeMAP_UNIVERSITY_SYSTEM =classtypeStudent,Course,CourseInfos = Course -m-> Student-set,University = Student-set >< CourseInfosvalue/* hasStudent проверяет, учится ли данный студент в указанном университете*/hasStudent : Student >< University -> Bool,/∗ hasCourse проверяет, читается ли данный курс в указанном университете*/hasCourse : Course >< University -> Bool,/∗ studOf возвращает множество студентов заданного университета,посещающих указанный курс ∗/studOf : Course >< University -~-> Student-set,/∗ attending возвращает множество курсов, которые посещает данный студентв указанном университете ∗/attending : Student >< University -~-> Course-set,/∗ newStud добавляет нового студента к числу студентов заданногоуниверситета ∗/newStud : Student >< University -~-> University,/∗ dropStud исключает указанного студента из числа студентов заданногоуниверситета ∗/dropStud : Student >< University -~-> University,/∗ newCourse добавляет новый курс с пустым множеством студентов к числукурсов заданного университета ∗/newCourse : Course >< University -~-> University,/∗ delCourse удаляет указанный курс из числа курсов заданного университета∗/delCourse : Course >< University -~-> UniversityendОпределите функции, сигнатура которых приведена в данном описании.Указания:• воспользуйтесь явным стилем описания функций и операциями надотображениями,• обратите внимание на тот факт, что использование в данной спецификациидетерминированного отображения для типа CourseInfos автоматическиобеспечиваетсвойствоуникальностикурсавпредложенноймоделе-ориентированной спецификации и, следовательно, отпадаетнеобходимость введения ограничения подтипа.34ГЛАВА 6.

АЛГЕБРАИЧЕСКИЕ СПЕЦИФИКАЦИИПонятие алгебраической спецификации. Классификация функций модели нагенераторы, модификаторы и обсерверы. Методика построения алгебраическойспецификации. RAISE метод разработки программ. Понятие уточнения моделей.Проверка согласованности моделей. Упражнения.Понятие алгебраической спецификацииАлгебраическая спецификация представляет собой частный случайаксиоматической спецификации, когда с помощью аксиом описываются свойстване какой-либо отдельной функции, а некоторой цепочки определяемых функций.

Вобщем случае такие аксиомы имеют вид:id(value_expr1, ..., value_exprn) is value_expr,где выражения value_expri сами, как правило, содержат вызовы функций. Например,f(g(x),x) is h(g(x)).При разработке спецификаций программной системы алгебраическиеспецификации используются на самом верхнем уровне абстракции, т.к., описываясвойства цепочек функций в терминах самих определяемых функций, не требуютуточнения типов и ограничиваются использованием только абстрактных типов.Построение алгебраической спецификации системы начинается соспецификации сигнатур, где объявляются типы данных (используются абстрактныетипы без конкретизации внутренней структуры) и сигнатуры функций.