Е.А. Кузьменкова - Формальная спецификация программ (Е.А. Кузьменкова - Формальная спецификация программ.pdf), страница 3

выбрать имя функции;2. выбрать тип:(a) аргументов,(b) результата,(c) отображения:• всюду вычислимая функция (может быть определена для всехзначений входных параметров),• частично вычислимая функция (необходимо предусловие);3. выбрать стиль описания:(a) явный (можно задать формулу вычисления результата),(b) неявный (можно описать связь входа и выхода посредством предиката),12(c) аксиоматический (может быть использован всегда, необходим валгебраических спецификациях).Упражнения1. Для обеспечения работы с комплексными числами описать:(a) тип ‘Complex’ для представления комплексных чисел,(b) константу ‘zero’ для представления комплексного числа 0 + 0i,(c) константу ‘c’, представляющую любое комплексное число вида x + xi;(d) функции ‘add’ и ‘mult’ для сложения и умножения комплексныхчисел,(e) функцию‘f’, возвращающую в качестве результата некотороекомплексное число, отличное от заданного.Указания:•в пунктах (b) и (d) воспользуйтесь явным (explicit) стилем описанияконстанты и функций, т.к.

здесь явно указано значение константы испособ получения результатов функций по их входным значениям;•в пунктах (c) и (e) следует использовать неявное (implicit) описаниеконстанты и функции, поскольку в условии не оговаривается явнозначение константы и способ получения результата по входномузначению;•в пунктах (c) и (d) для упрощения записи удобно воспользоватьсяконструкцией let. С помощью этой конструкции, например, дляпункта (c) факт равенства действительной и мнимой частейкомплексного числа c можно записать так:let (x, y) = c in x = y end2. Пусть система координат описывается следующим образом:SYSTEM_OF_COORDINATES=classtypePosition = Real × Realvalueorigin : Position = (0.0,0.0),distance : Position × Position → Realdistance((x1, y1),(x2, y2)) ≡((x2 – x1)↑2.0 + (y2 – y1)↑2.0)↑0.5endЗдесь тип ‘Position’ предназначен для описания координат точек наплоскости, константа ‘origin’ задает начало координат, функция ‘distance’определяет способ вычисления расстояния между двумя точками.

Обратитевнимание на то, что при описании константы ‘origin’ и функции ‘distance’использован явный стиль описания (explicit definition), т.к. указанонепосредственное значение константы и формула для вычисления расстояния.13Используя заданную спецификацию описать:(a) тип ‘Circle’ для описания окружности по ее центру и радиусу;(b) функцию ‘on_circle’, определяющую лежит ли точка с заданнымикоординатами на заданной окружности;(c) окружность с радиусом 3.0 и центром в начале координат;(d) константу ‘pos’ для представления произвольной точки, лежащей назаданной окружности.Указания:• в пункте (a) опишите вспомогательные типы ‘Center’ и ‘Radius’для представления центра окружности и ее радиуса соответственно, дляописания типа ‘Center’ используйте тип ‘Position’, для типа‘Radius’ воспользуйтесь следующим описанием:Radius = {| r : Real • r ≥ 0.0 |}, задающим подтип действительных чисел снеотрицательными значениями;• в пунктах (b) и (c) следует воспользоваться явным стилем описания(explicit definition), можно также использовать конструкцию let длядостижения большей наглядности записи;• в пункте (d) используйте неявный (implicit) стиль описания константы.3.

Определить функцию‘max’, возвращающую значение максимума из двухцелых чисел, используя один из следующих стилей описания:(a) явный,(b) неявный,(c) аксиоматический.Указания:• воспользуйтесь общей схемой определения функции, изложенной впункте 1.2.3.5;• для удобства записи используйте условное выражение языка RSL видаif логическое_выражение then выражение else выражение end.4. Определить функцию‘approx_sqrt’, которая с заданной точностью ‘eps’(положительное вещественное число) находит приближённое значение корняквадратного из неотрицательного вещественного числа.

Возвращаемыйфункцией результат должен быть таким, чтобы точное значение квадратногокорня square_root(x)лежаловполуоткрытоминтервале[approx_sqrt(x,eps),approx_sqrt(x,eps) + eps[.Указания:• здесь следует использовать неявный стиль описания, т.к. в постановкезадачи оговариваются только соотношения между входными ивыходными параметрами и не уточняется алгоритм вычисленияприближенного значения;• обратите внимание на то, что функция определена не для всех значенийвходных параметров, т.е. является частично вычислимой.145. Рассмотрим следующее описание функции:valuef : Int −∼→ Intf(x) ≡ f(x)Какие из перечисленных ниже функций удовлетворяют данному описанию?(a) valuef : Int −∼→ Intf(x) ≡ chaos(b) valuef : Int −∼→ Intf(x) ≡ 1(c) valuef : Int → Intf(x) ≡ 1Указания:• запишите исходное определение функции в аксиоматическом стиле и спомощью эквивалентных преобразований упростите полученныйрезультат;• воспользуйтесь тем фактом, что частично вычислимые функциивключают в себя всюду вычислимые функции.1.3.МножестваЦель данного раздела - познакомить читателя с принятыми в RSLспособами описания множеств и основными операциями над множествами.Раздел содержит упражнения по использованию абстракции множеств вмоделеориентированных спецификациях.1.3.1.

Понятие множестваМножеством называется неупорядоченный набор различных значенийодного и того же типа. Например:{1,3,5}{″Mary″,″John″,″Peter″}При этом, как видно из определения множества, записи {1,3,5}, {5,3,1} и{3,5,1,1} определяют одно и то же множество.Для описания типа множества в RSL предусмотрена конструкцияtype_expr-set для конечных множеств и type_expr-infset для бесконечных,15при этом type_expr задает тип входящих в множество элементов.

Так,значениями типа Bool-set являются следующие конечные множества:{}{true}{false}{true, false},причем сюда включается пустое множество {}.Тип type_expr-infset представляет как конечные, так и бесконечныемножества, состоящие из элементов типа type_expr. Следовательно, длялюбого типа T тип T-set является подтипом T-infset. Например, типNat-infset содержит все конечные (в том числе и пустое) и бесконечныемножества натуральных чисел.Для работы с множествами в RSL определены следующие операции:∪,∩,\,∈,∉,⊂,⊆,⊃,⊇ и card, кроме того можно использовать отношения = и ≠.Операция card вычисляет размер конечного множества, т.е.

количество егоэлементов:card : T-infset −∼→ NatПри применении к бесконечному множеству card возвращает chaos.Например:card {1,4,56} = 3card {} = 0card {n | n : Nat} ≡ chaos1.3.2. Способы определения множествКонечное множество может быть задано путем непосредственногоперечисления его элементов, как в приведенных выше примерах, в этом случаевыражение, определяющее значение множества, имеет вид {v1,...,vn}, где 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}.16Упражнения1. Написать выражение, задающее значение множества, элементами которогоявляются нечетные числа в диапазоне от 0 до 10.Указания:используйте два способа задания значения множества: непосредственноеперечисление его элементов и сокращенное выражение.2.Пусть база данных университета описана следующим образом (для простотыкомментарии приведены на русском языке):schemeUNIVERSITY_SYSTEM =classtypeStudent,Course,CourseInfo = Course × Student-set,University = Student-set × CourseInfo-setvalue/∗ allStudents возвращает множество всех студентов, обучающихся вданном университете ∗/allStudents : University → Student-set,/∗ hasCourse проверяет, читается ли данный курс в данномуниверситете∗/hasCourse : Course × University → Bool,/∗ numberOK возвращает значение true, если любой читаемый вуниверситете курс посещает не менее 5 и не более 100 студентов ∗/numberOK : University → Bool,/∗ studOf возвращает множество студентов заданного университета,посещающих заданный курс ∗/studOf : Course × University −∼→ Student-set,/∗ attending возвращает множество курсов, которые посещаетзаданный студент в указанном университете ∗/attending : Student × University −∼→ Course-set,/∗ newStud добавляет нового студента к числу студентов заданногоуниверситета ∗/newStud : Student × University −∼→ University,/∗ dropStud исключает указанного студента из числа студентовзаданного университета ∗/dropStud : Student × University −∼→ UniversityendОпределите функции, сигнатура которых приведена в данном описании.17Указания:воспользуйтесь явным стилем описания функций и операциями надмножествами.3.

Почему некоторые из перечисленных выше функций частично вычислимы?1.4.СпискиЦель данного раздела - познакомить читателя с принятыми в RSLспособами описания списков и основными операциями над списками. Разделсодержит упражнения по использованию списков в спецификациях программ.1.4.1. Понятие спискаСписком называется последовательность значений одного и того же типа,например:〈1,3,3,1,5〉〈true,false,true〉Для списков допустимо использование отношений = и ≠. Порядок следованияэлементов в списке существенен, т.е. списки 〈1,3,5〉 и 〈5,3,1〉 являютсяразличными (〈1,3,5〉 ≠ 〈5,3,1〉). Кроме того, допускается повторное вхождениеэлементов в список (как в рассмотренных выше примерах), причем〈1,3,3,1,5〉 ≠ 〈1,3,5〉.Для описания конечных списков в RSL используется конструкция видаtype_expr*, где type_expr задает тип элементов списка.

Например, типBool* описывает любой конечный список (в том числе и пустой) из булевскихзначений. Конструкция type_exprω задает тип как конечных, так ибесконечных списков из элементов типа type_expr. Таким образом, для любоготипа T, T* является подтипом Tω.1.4.2. Способы определения списковДля списков применяются те же способы определения значений, что и длямножеств. Так, значение конечного списка может быть задано путемнепосредственного перечисления его элементов. В этом случае значение спискаопределяется выражением вида 〈v1,...,vn〉, где n≥0 и все vi являютсявыражениями одного и того же типа, в частности, 〈〉 задает пустой список.Конечный список из последовательных целых чисел можно задать, указавдиапазон изменения значений элементов списка, т.е. выражением вида 〈v1..v2〉,где v1 и v2 задают соответственно нижнюю и верхнюю границы диапазона,причем при v1 > v2 список пуст.Использование такого способа записи иллюстрируют следующие примеры:〈3..7〉 =〈3,4,5,6,7〉〈3..3〉 = 〈3〉〈3..2〉 = 〈〉18Значение списка можно задать также по аналогии с множествами и спомощью так называемого сокращенного выражения (comprehended listexpression),имеющеговид 〈 value_expr | list_limitation 〉.