[3 +> true,3 +> false].

Способы определения отображений

Для определения отображений в RSL используются те же способы, что и для множеств и списков, а именно: непосредственное перечисление элементов и сокращенное выражение. Первый способ может применяться для конечных отображений, в этом случае отображение задается выражением вида:

[v₁ +> w₁,…,v_n +> w_n],

где n  0 (в частности, при n  0 имеем пустое отображение []). Здесь выражения v_i задают значения ключей и w_i – сопоставляемых им значений. Именно этот способ был использован во всех рассмотренных ранее примерах.

Сокращенное выражение (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_expr₁(value_expr₂),  где  value_expr₁ является выражением, определяющим данное отображение, value_expr₂ – выражение для вычисления значения некоторого элемента из домена отображения. Например:

[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,

где символ ^ означает недетерминированный (внутренний) выбор из двух указанных значений. Для значений, не принадлежащих домену отображения, эффект применения отображения не определен, т.е. соответствующее выражение возвращает chaos:

[1 +> 2, 2 +> 3](5) = chaos

Операции над отображениями

Над отображениями определены следующие операции:

dom : (T₁ –m-> T₂) -> T₁-infset

rng : (T₁ –m-> T₂) -> T₂-infset

!! : (T₁ –m-> T₂) >< (T₁ –m-> T₂) -> (T₁ –m-> T₂) 

union : (T₁ –m-> T₂) >< (T₁ –m-> T₂) -> (T₁ –m-> T₂)

\ : (T₁ –m-> T₂) >< T₁-infset -> (T₁ –m-> T₂)

/ : (T₁ –m-> T₂) >< T₁-infset -> (T₁ –m-> T₂)

# : (T₂ –m-> T₃) >< (T₁ –m-> T₂) -> (T₁ –m-> T₃)

Кроме того для отображений определены операции = и ~=.

Операции dom и rng возвращают в качестве результата соответственно домен и область значений отображения, причем в зависимости от вида отображения эти множества могут быть конечными или бесконечными. Для любого отображения m верно соотношение:

rng m is {m(x) | x : T₁ :- 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 : T₁, w : T₂ :- 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 просто объединяет наборы пар двух заданных отображений, например:

[3 +> true, 5 +> false] union [5 +> true]  [3 +> true, 5 +> false, 5 +> true]

Эта операция может привести к недетерминизму (как в рассмотренном выше примере), поэтому во избежание возникновения недетерминизма обычно применяется к отображениям с непересекающимися доменами.

Операции ограничения отображений \ и / позволяют изменять домены отображений, а именно: \ удаляет из домена отображения указанное множество, / , напротив, оставляет в домене только те элементы, которые входят в указанное множество. Более точно определение этих операций выглядит следующим образом:

m \ s  [v +> m(v)  v : T₁ :- v isin (dom m) \ s]

m / s  [v +> m(v)  v : T₁ :- 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]

Операция # позволяет осуществлять композицию двух отображений, т.е. для отображений m₁ и m₂ она определяется так:

m₁ # m₂  [v +> m₁(m₂(v))  v : T₁ :- v isin dom m₂ /\ m₂(v) isin dom m₁]

Например:

[3 +> true, 5 +> false] # [Klaus +> 3, John +> 7]  [Klaus +> true]

[3 +> true] # [Klaus +> 5]  [ ]

Упражнения

1. Определить отображение, сопоставляющее:

(a) каждому нечетному натуральному числу, не превосходящему 30, его остаток от деления на 3,

1. каждой паре натуральных чисел остаток от деления первого числа на второе (первое число должно быть меньше 50),

2. каждому натуральному числу, не превосходящему 20, все его делители,

3. каждому натуральному числу ближайшее, не превосходящее его, число, являющееся полным квадратом,

4. каждому натуральному числу n, не превосходящему 30, все простые числа из диапазона [2, n]; применить построенное отображение к n = 1, 10, 50.

Указания: используйте сокращенное выражение для определения отображений.

1. Пример использования абстракции отображений в моделе-ориентированной спецификации. Пусть база данных университета описана следующим образом:

scheme

MAP_UNIVERSITY_SYSTEM =

class

type

Student,

Course,

CourseInfos = Course ‑m‑> Student-set,

University = Student-set >< CourseInfos

value

/* 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 -~-> University

end

Определите функции, сигнатура которых приведена в данном описании.

Указания:

• воспользуйтесь явным стилем описания функций и операциями над отображениями,

• обратите внимание на тот факт, что использование в данной спецификации детерминированного отображения для типа CourseInfos автоматически обеспечивает свойство уникальности курса в предложенной моделе‑ориентированной спецификации и, следовательно, отпадает необходимость введения ограничения подтипа.

ГЛАВА 6. АЛГЕБРАИЧЕСКИЕ СПЕЦИФИКАЦИИ

Понятие алгебраической спецификации. Классификация функций модели на генераторы, модификаторы и обсерверы. Методика построения алгебраической спецификации. RAISE метод разработки программ. Понятие уточнения моделей. Проверка согласованности моделей. Упражнения.

Понятие алгебраической спецификации

Алгебраическая спецификация представляет собой частный случай аксиоматической спецификации, когда с помощью аксиом описываются свойства не какой-либо отдельной функции, а некоторой цепочки определяемых функций. В общем случае такие аксиомы имеют вид:

id(value_expr₁, ..., value_expr_n) is value_expr,

где выражения value_expr_i сами, как правило, содержат вызовы функций. Например, f(g(x),x) is h(g(x)).

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

Построение алгебраической спецификации системы начинается со спецификации сигнатур, где объявляются типы данных (используются абстрактные типы без конкретизации внутренней структуры) и сигнатуры функций. При этом среди объявленных типов особо выделяется тип, с помощью которого моделируется реализация целевой системы, - целевой тип.

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

Можно предложить следующую спецификацию сигнатур для данной системы:

DATABASE =

class

type Database, Key, Data

value