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

Определить функцию approx_sqrt, которая с заданной точностью eps (положительное вещественное число) находит приближённое значение корняквадратного из неотрицательного вещественного числа. Возвращаемый18функцией результат должен быть таким, чтобы точное значение квадратногокорня лежало в полуоткрытом интервале:[approx_sqrt(x,eps), approx_sqrt(x,eps) + eps).Указания:• здесь следует использовать неявный стиль описания, т.к.

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

является частично вычислимой.8. Дана явная спецификация функции, предложить неявную спецификациюфункции, эквивалентной данной:(a) value(b)F1 : Int >< Int >< Int -> Int >< IntF1(a, b, c) isif a < b then (a * c, b - a)elsif a > b then (a – b, b * c)else (a, b)endvalueF2 : Nat >< Nat >< Nat -> Nat >< NatF2(a, b, c) is(if a + b > c then c else a + b end,a * b * (if с > 0 then c else 0 –c end))19ГЛАВА 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 содержит все конечные(в том числе и пустое) и бесконечные множества натуральных чисел.Способы определения множествКонечное множество может быть задано путем непосредственногоперечисления его элементов (именно этот способ был использован в приведенныхвыше примерах), в этом случае выражение, определяющее значение множества,имеет вид {v1,...,vn}, где n≥0. Кроме того, для конечных множеств,образованных из целых чисел, возможно также использование диапазона длязадания значения множества, причем левая граница диапазона не должнапревышать его правую границу (в противном случае множество будет пусто).Например, выражение {3 .. 7} задает множество {3,4,5,6,7}, {3 ..

3} –множество из единственного элемента {3} и  {3 .. 2} – пустое множество {}.20Более общей формой выражения, определяющего значение как конечного, таки бесконечного множества, является выражение вида:{ 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} = 3card {} = 0card {n | n : Nat} ≡ chaosУпражнения1.

Определить множество, элементами которого являются:(a) нечетные числа в диапазоне от 0 до 10,(b) простые числа в диапазоне от 2 до 20.Указания: используйте два способа задания значения множестванепосредственное перечисление его элементов и сокращенное выражение.-212.

Вычислить значение выражения:card { n | n : Nat :- 30 \ n = 0}3. Написать RSL выражение для вычисления количества точек с целочисленнымикоординатами, попадающими внутрь круга с центром в начале координат ирадиусом 5.Указания: определите множество координат соответствующих точек и найдитеколичество его элементов.4. Определить функцию:(a) max, возвращающую максимум из значений элементов непустогомножества из целых чисел,(b) choose, возвращающую некоторый элемент непустого множества изэлементов типа Т.Указания:•используйте неявный стиль описания функций,•обратите внимание на то, что обе функции определены не для всехзначений входного параметра, т.е.

являются частично вычислимыми.5. Пример использования абстракции множеств в моделе-ориентированнойспецификации. В базе данных университета содержится информация остудентах, обучающихся в этом университете, и читаемых им курсах. Пустьбаза данных университета описана следующим образом:schemeUNIVERSITY_SYSTEM =classtypeStudent,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,22/∗ dropStud исключает указанного студента из числа студентов заданногоуниверситета ∗/dropStud : Student >< University -~-> University,/∗ newCourse добавляет новый курс с пустым множеством студентов к числукурсов заданного университета ∗/newCourse : Course >< University -~-> University,/∗ delCourse удаляет указанный курс из числа курсов заданного университета∗/delCourse : Course >< University -~-> Universityend(a) Написать явное определение функций, сигнатура которых приведена вданном описании.(b) Описать неявную спецификацию функции studOf.(c) Почему некоторые из перечисленных выше функций частично вычислимы?Указания:• обратите внимание на необходимость введения ограничения подтипа приопределении типа University для проверки того свойства, что для любогочитаемого в университете курса в базе данных должно быть зафиксированоединственное множество посещающих этот курс студентов (свойствоуникальности курса),• в пункте (а) воспользуйтесь явным стилем описания функций и операцияминад множествами.23ГЛАВА 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.Способы определения списковДля списков применяются те же способы определения значений, что и длямножеств. Так, значение конечного списка может быть задано путемнепосредственного перечисления его элементов. В этом случае значение спискаопределяется выражением вида <.v1,...,vn.>, где n≥0 и все vi являютсявыражениями одного и того же типа, в частности, <..> задает пустой список. Вприведенных выше примерах был использован именно этот способ.