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

Предусловие задается предикатом,зависящим от входных параметров определяемой функции.Дальнейшее определение функции подобно рассмотренному ранееопределению констант может производиться в одном из следующих стилей:•явном (эксплицитном, explicit),•неявном (имплицитном, implicit),• аксиоматическом.Выбор конкретного стиля спецификации зависит от специфики решаемой задачи.Явное описание функцийОписание функции в явном стиле (операционная спецификация)ориентировано на описание конкретного алгоритма и используется в том случае,когда явно задаётся способ преобразования входных параметров в выходные.Примером явного описания всюду вычислимой функции может служитьследующий фрагмент RSL спецификации:valuef : Int -> Intf(x) is x + 1В качестве примера описания частично вычислимой функции в явном стилерассмотрим функцию p(x), вычисляющую значение 1/x:valuep : Real -~-> Realp(x) is 1.0/xpre x ~= 0.0Последняя строка данного описания содержит предусловие, представляющее собойпредикат, накладывающий ограничение на значения входного параметра.14Неявное описание функцийОписание функции в неявном стиле (контрактная спецификация) нацелено наописание свойств результата функции, которые фиксируются в виде некоторогопредиката в постусловии определяемой функции.

Неявная спецификация,абстрагируясь от конкретного способа получения результата, во главу угла ставитформализацию отношений, связывающих между собой входные и выходныепараметры, т.е. здесь описывается не сам алгоритм, а эффект его применения.Данный стиль описания соответствует более высокому уровню абстракции, чемявная спецификация, поскольку конкретный алгоритм преобразования неуказывается и может быть уточнен в дальнейшем путем построения явнойспецификации определяемой функции. При этом для одной и той же неявнойспецификации можно предложить, вообще говоря, разные алгоритмы, эффектприменения которых удовлетворяет указанной спецификации. При разработкеспецификаций функций этап построения их неявных спецификаций как правилопредшествует этапу построения явных спецификаций.Ниже приведены примеры описания в неявном стиле всюду вычислимойфункции f(x), возвращающей в качестве результата некоторое целое число,превосходящее входное значение:valuef : Int -> Intf(x) as r post r > xи частично вычислимой функции square_root(x) для нахождения значенияквадратного корня:valuesquare_root : Real -∼->.

Realsquare_root(x) as spost s ∗ s = x /\ s >= 0.0pre x >= 0.0Причем, как видно из примеров, конкретный алгоритм получения результатаостается в обоих случаях за рамками рассмотрения, описываются лишь свойстварезультата.Аксиоматическое описание функцийПри использовании аксиоматического стиля описания функции предлагаетсянекоторый набор аксиом, определяющих свойства данной функции.Аксиоматическая спецификация может применяться с одинаковым успехом и дляописания способа получения результата, и для описания свойств самого результатавыполнения функции. Поэтому как для явного, так и для неявного описаний всегдаможно предложить эквивалентное описание в аксиоматическом стиле.

Кроме тогоданный стиль является единственно возможным при построении алгебраическихспецификаций, где аксиомы описывают свойства цепочек функций и имеютспецифический вид (например, f(g(x), x) is h(x)), т.е. в качестве аргумента функциидопускается использование обращения к функции.15В качестве примеров приведем аксиоматическое описание всюду вычислимойфункции f(x), эквивалентное рассмотренному выше явному описанию той жефункции:valuef : Int -> Intaxiom all x : Int :- f(x) is x + 1и аксиоматическую спецификацию частично вычислимой функции square_root(x), эквивалентную ее неявной спецификации, также рассмотреннойранее:valuesquare_root : Real -∼-> Realaxiomall x : Real :-x >= 0.0 =>exists s : Real :- square_root(x) = s /\ s ∗ s = x /\ s >= 0.0Схема определения функцииПодводя итог вышесказанному, можно предложить следующую схемуопределения функции:1.

Описать сигнатуру функции:• выбрать имя функции;• выбрать тип:(a) аргументов,(b) результата,(c) отображения:- всюду вычислимая функция (может быть определена для всехзначений входных параметров),- частично вычислимая функция (необходимо предусловие);2.выбрать стиль спецификации:• явный (можно задать способ вычисления результата),• неявный (можно описать связь входа и выхода посредством предиката),• аксиоматический (может быть использован всегда, необходим валгебраических спецификациях).Упражнения1. Для обеспечения работы с точками на плоскости описать тип дляпредставления:всех точек на плоскости, принадлежащих первому квадранту и лежащихвыше прямой y=x,(b) всех точек с целочисленными координатами, лежащих внутри круга сцентром в начале координат и радиусом 5.(a)Указания: используйте декартово произведение и аппарат определения подтипов.162.

Используя явный стиль спецификации, определить функцию:(a)(b)is_even для проверки заданного числа на четность,is_a_prime, которая проверяет, является ли ее аргумент простым числом.Указания: в пункте (a) можно использовать операцию \ (остаток от деления) иливоспользоваться квантифицированным выражением.3. Определить функцию max, возвращающую значение максимума из двухцелых чисел, используя один из следующих стилей описания:(a) явный,(b) неявный,(c) аксиоматический.Указания:• воспользуйтесь приведенной в этой главе общей схемой определенияфункции;• для удобства записи в пунктах (a) и (c) используйте условное выражениеязыка RSL.4.

Для обеспечения работы с комплексными числами описать:(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 end5.

Пусть задана следующая спецификация системы координат:scheme SYSTEM_OF_COORDINATES=classtypePosition = Real >< Realvalue17origin : Position = (0.0,0.0),distance : Position >< Position -> Realdistance((x1, y1),(x2, y2)) is((x2 – x1)**2.0 + (y2 – y1)**2.0)**0.5endЗдесь тип Position предназначен для описания координат точек наплоскости, константа origin задает начало координат, функция distance определяет способ вычисления расстояния между двумя точками. Обратитевнимание на то, что при описании константы origin и функции distance использован явный стиль описания, т.к.

указано непосредственное значениеконстанты и формула для вычисления расстояния.Дополнить заданную спецификацию определением:(a) типа Circle для описания окружности по ее центру и радиусу;(b) функции on_circle, определяющей, лежит ли точка с заданнымикоординатами на заданной окружности;(c) окружности с радиусом 3.0 и центром в начале координат;(d) константы pos для представления произвольной точки, лежащей назаданной окружности.Указания:• в пункте (a) определите вспомогательные типы Center и Radius дляпредставления центра окружности и ее радиуса соответственно, дляопределения типа Center используйте тип Position, для типа Radius воспользуйтесь следующим описанием:Radius = {| r : Real :- r >= 0.0 |},задающим подтип действительных чисел с неотрицательными значениями;• в пунктах (b) и (c) следует воспользоваться явным стилем описания функциии константы, можно также использовать конструкцию  let длядостижения большей наглядности записи;• в пункте (d) используйте неявный стиль описания константы.6.

Для обеспечения работы с рациональными числами предложить спецификациюсхемы RATIONAL_NUMBERS, содержащей определения:(a) типа Rational для представления рациональных чисел;(b) функции less, которая сравнивает два рациональных числа и возвращаетtrue, если первое число меньше второго;(c) функции add для сложения двух рациональных чисел;(d) функции max для определения максимума из двух рациональных чисел;(e) функции check, которая проверяет, является ли заданное рациональноечисло несократимой дробью.Указания: используйте явный стиль спецификации.7.