Указания:

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

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

1. Дана явная спецификация функции, предложить неявную спецификацию функции, эквивалентной данной:

1. value

F1 : Int >< Int >< Int -> Int >< Int

F1(a, b, c) is if a < b then (a * c, b - a)

elsif a > b then (a – b, b * c)

else (a, b)

end

1. value

F2 : Nat >< Nat >< Nat -> Nat >< Nat

F2(a, b, c) is (if a + b > c then c else a + b end,

a * b * (if с > 0 then c else 0 –c end))

ГЛАВА 3. ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ-ОРИЕНТИРОВАННЫХ СПЕЦИФИКАЦИЯХ. МНОЖЕСТВА

Понятие множества, конечные и бесконечные множества. Способы определения множеств. Операции над множествами в RSL. Использование абстракции множеств в моделе-ориентированных спецификациях. Упражнения.

Понятие множества

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

{1,3,5}

{0.0, 1.5, 4.7}

{Mary,John,Peter}

Из определения множества следуют два основных свойства множества:

• все элементы множества различны между собой,

• на множестве не задано отношение порядка.

Таким образом, выражения {1,3,5}, {5,3,1} и {3,5,1,1} определяют одно и то же множество.

В RSL различаются конечные и бесконечные множества. Для описания типа множества в RSL предусмотрены типовые операции -set и -infset, с помощью которых строится составной тип T-set для описания конечных множеств из элементов типа T и T-infset – для бесконечных множеств из элементов того же типа. Так, значениями типа Bool-set являются следующие конечные множества:

{}

{true}

{false}

{true, false},

причем сюда включается пустое множество {}.

Тип T-infset представляет как конечные, так и бесконечные множества, состоящие из элементов типа T. Следовательно, для любого типа T тип T-set является подтипом T-infset. Например, тип Nat-infset содержит все конечные (в том числе и пустое) и бесконечные множества натуральных чисел.

Способы определения множеств

Конечное множество может быть задано путем непосредственного перечисления его элементов (именно этот способ был использован в приведенных выше примерах), в этом случае выражение, определяющее значение множества, имеет вид {v₁,...,v_n}, где n0. Кроме того, для конечных множеств, образованных из целых чисел, возможно также использование диапазона для задания значения множества, причем левая граница диапазона не должна превышать его правую границу (в противном случае множество будет пусто). Например, выражение {3 .. 7} задает множество {3,4,5,6,7}, {3 .. 3} – множество из единственного элемента {3} и  {3 .. 2} – пустое множество {}.

Более общей формой выражения, определяющего значение как конечного, так и бесконечного множества, является выражение вида:

{ value_expr  set_limitation },

называемое сокращенной (compehended) записью множества или сокращенным выражением. При этом выражение value_expr задает формулу для вычисления значений элементов множества, конструкция set_limitation определяет тип элементов множества и возможные ограничения на значения этих элементов, заданные в виде некоторого предиката. Примером такой формы записи может служить выражение {2n  n : Nat :- n <= 3}, с помощью которого задается конечное множество {0, 2, 4, 6} или выражение {2n  n : Nat}, определяющее бесконечное множество из четных натуральных чисел.

Операции над множествами

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

inter – пересечение (),

union – объединение (),

\ - вычитание,

isin, ~isin – проверка принадлежности (или не принадлежности) множеству (,),

<<, <<=, >>, >>= - проверка, является ли одно множество подмножеством другого (, , , ),

card – вычисление количества элементов множества,

кроме того можно использовать операции = и ~=.

Операция card вычисляет размер конечного множества, т.е. количество его элементов:

card : T-infset --> Nat

При применении к бесконечному множеству card возвращает chaos. Например:

card {1, 4, 56} = 3

card {} = 0

card {n  n : Nat}  chaos

Упражнения

1. Определить множество, элементами которого являются:

1. нечетные числа в диапазоне от 0 до 10,

2. простые числа в диапазоне от 2 до 20.

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

1. Вычислить значение выражения:

card { n  n : Nat :- 30 \ n = 0}

1. Написать RSL выражение для вычисления количества точек с целочисленными координатами, попадающими внутрь круга с центром в начале координат и радиусом 5.

Указания: определите множество координат соответствующих точек и найдите количество его элементов.

1. Определить функцию:

1. max, возвращающую максимум из значений элементов непустого множества из целых чисел,

2. choose, возвращающую некоторый элемент непустого множества из элементов типа Т.

Указания:

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

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

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

scheme

UNIVERSITY_SYSTEM =

class

type

Student,

Course,

CourseInfo = Course >< Student-set,

University = {| (ss, cis) : Student-set >< CourseInfo-set :- is_wf(ss, cis) |}

value

 is_wf осуществляет проверку на «хорошо сформированную» базу данных, проверяя выполнение свойства уникальности курса 

is_wf :- Student-set >< CourseInfo-set -> Bool,

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

1. Написать явное определение функций, сигнатура которых приведена в данном описании.

2. Описать неявную спецификацию функции studOf.

3. Почему некоторые из перечисленных выше функций частично вычислимы?

Указания:

• обратите внимание на необходимость введения ограничения подтипа при определении типа University для проверки того свойства, что для любого читаемого в университете курса в базе данных должно быть зафиксировано единственное множество посещающих этот курс студентов (свойство уникальности курса),

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

ГЛАВА 4. ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ-ОРИЕНТИРОВАННЫХ СПЕЦИФИКАЦИЯХ. СПИСКИ

Понятие списка, конечные и бесконечные списки. Способы определения списков. Операции над списками. Выражение case. Использование абстракции списков в моделе-ориентированнных спецификациях. Упражнения

Понятие списка

Под списком понимается последовательность значений одного и того же типа, например:

<.1, 3, 3, 1, 5.>

<.true, false, true.>

<.3.14, 0.15.>

Отсюда следуют два основных свойства списка:

• порядок следования элементов в списке определен и существенен,

• допускается повторное вхождение элементов в список.

Таким образом, выражения <.1, 3, 5.>, <.5, 3, 1.> и <.1, 3, 3, 1, 5.> определяют три разных списка.

В RSL различаются конечные и бесконечные списки. Для описания типа списка предусмотрены типовые операции -list и -inflist, с помощью которых строится составной тип T-list для описания конечных списков из элементов типа T и T-inflist – для бесконечных списков из элементов того же типа. Например, значениями типа Bool-list являются все конечные списки (в том числе и пустой) из булевских значений.

Выражение T-inflist  задает тип как конечных, так и бесконечных списков из элементов типа T. Следовательно, для любого типа T тип T- list является подтипом T-inflist.

Способы определения списков

Для списков применяются те же способы определения значений, что и для множеств. Так, значение конечного списка может быть задано путем непосредственного перечисления его элементов. В этом случае значение списка определяется выражением вида <.v₁,...,v_n.>, где n0 и все v_i являются выражениями одного и того же типа, в частности, <..> задает пустой список. В приведенных выше примерах был использован именно этот способ. Конечный список из последовательных целых чисел можно задать, указав диапазон изменения значений элементов списка, т.е. выражением вида <.v₁..v₂.>, где v₁ и v₂ задают соответственно нижнюю и верхнюю границы диапазона, причем при v₁  v₂ список пуст.

Использование такого способа записи иллюстрируют следующие примеры:

<.3..7.> <.3, 4, 5, 6, 7.>

<.3..3.>  <.3.>

<.3..2.>  <..>

Значение списка можно задать также по аналогии с множествами и с помощью так называемого сокращенного выражения (comprehended list expression), имеющего вид <. value_expr  list_limitation .>. Этот способ применяется в том случае, когда новый список строится на основе какого-то уже существующего. Здесь value_expr определяет общую формулу для вычисления значений элементов нового списка, list_limitation задает базовый список, на основе которого строится данный, с возможным указанием некоторого предиката для отбора элементов из базового списка.

Например, в выражении:

<.2n  n in <.0 .. 3.>.>