методичка (Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL), страница 3

all x : T₁ :- exists! y : T₂ :- f(x) is y

Сигнатура функции f в этом случае имеет вид:

f : T₁ -> T₂

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

Функция f, отображающая значения типа T₁ в значения типа T₂, является частично вычислимой (partial function), если существует такое значение v типа T₁, для которого вычисление f(v) может либо вообще не завершиться (в этом случае f(v) is chaos), либо привести к недетерминированному результату, когда различные вхождения выражения f(v) могут возвращать разные значения.

Сигнатура частично вычислимой функции f имеет вид:

f : T₁ --> T₂

Частично вычислимые функции включают в себя всюду вычислимые функции.

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

Дальнейшее определение функции подобно рассмотренному ранее определению констант может производиться в одном из следующих стилей:

• явном (эксплицитном, explicit),

• неявном (имплицитном, implicit),

• аксиоматическом.

Выбор конкретного стиля спецификации зависит от специфики решаемой задачи.

Явное описание функций

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

value

f : Int -> Int

f(x) is x + 1

В качестве примера описания частично вычислимой функции в явном стиле рассмотрим функцию p(x), вычисляющую значение 1/x:

value

p : Real -~-> Real

p(x) is 1.0/x

pre x ~= 0.0

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

Неявное описание функций

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

Ниже приведены примеры описания в неявном стиле всюду вычислимой функции f(x), возвращающей в качестве результата некоторое целое число, превосходящее входное значение:

value

f : Int -> Int

f(x) as r post r > x

и частично вычислимой функции square_root(x) для нахождения значения квадратного корня:

value

square_root : Real -->. Real

square_root(x) as s

post s  s = x /\ s >= 0.0

pre x >= 0.0

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

Аксиоматическое описание функций

При использовании аксиоматического стиля описания функции предлагается некоторый набор аксиом, определяющих свойства данной функции. Аксиоматическая спецификация может применяться с одинаковым успехом и для описания способа получения результата, и для описания свойств самого результата выполнения функции. Поэтому как для явного, так и для неявного описаний всегда можно предложить эквивалентное описание в аксиоматическом стиле. Кроме того данный стиль является единственно возможным при построении алгебраических спецификаций, где аксиомы описывают свойства цепочек функций и имеют специфический вид (например, f(g(x), x) is h(x)), т.е. в качестве аргумента функции допускается использование обращения к функции.

В качестве примеров приведем аксиоматическое описание всюду вычислимой функции f(x), эквивалентное рассмотренному выше явному описанию той же функции:

value

f : Int -> Int

axiom all x : Int :- f(x) is x + 1

и аксиоматическую спецификацию частично вычислимой функции square_root(x), эквивалентную ее неявной спецификации, также рассмотренной ранее:

value

square_root : Real --> Real

axiom

all x : Real :-x >= 0.0 =>

exists s : Real :- square_root(x) = s /\ s  s = x /\ s >= 0.0

Схема определения функции

Подводя итог вышесказанному, можно предложить следующую схему определения функции:

1. Описать сигнатуру функции:

• выбрать имя функции;

• выбрать тип:

1. аргументов,

2. результата,

3. отображения:

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

- частично вычислимая функция (необходимо предусловие);

1. выбрать стиль спецификации:

• явный (можно задать способ вычисления результата),

• неявный (можно описать связь входа и выхода посредством предиката),

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

Упражнения

1. Для обеспечения работы с точками на плоскости описать тип для представления:

1. всех точек на плоскости, принадлежащих первому квадранту и лежащих выше прямой y=x,

2. всех точек с целочисленными координатами, лежащих внутри круга с центром в начале координат и радиусом 5.

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

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

1. is_even для проверки заданного числа на четность,

2. is_a_prime, которая проверяет, является ли ее аргумент простым числом.

Указания: в пункте (a) можно использовать операцию \ (остаток от деления) или воспользоваться квантифицированным выражением.

1. Определить функцию max, возвращающую значение максимума из двух целых чисел, используя один из следующих стилей описания:

1. явный,

1. неявный,

2. аксиоматический.

Указания:

• воспользуйтесь приведенной в этой главе общей схемой определения функции;

• для удобства записи в пунктах (a) и (c) используйте условное выражение языка RSL.

1. Для обеспечения работы с комплексными числами описать:

1. тип Complex для представления комплексных чисел,

2. константу zero для представления комплексного числа 0 + 0i,

3. константу c, представляющую любое комплексное число вида x + xi;

4. функции add и mult для сложения и умножения комплексных чисел,

5. функцию f, возвращающую в качестве результата некоторое комплексное число, отличное от заданного.

Указания:

• в пунктах (b) и (d) воспользуйтесь явным (explicit) стилем описания константы и функций, т.к. здесь явно указано значение константы и способ получения результатов функций по их входным значениям;

• в пунктах (c) и (e) следует использовать неявное (implicit) описание константы и функции, поскольку в условии не оговаривается явно значение константы и способ получения результата по входному значению;

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

let (x, y) = c in x = y end

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

scheme SYSTEM_OF_COORDINATES=

class

type

Position = Real >< Real

value

origin : Position = (0.0,0.0),

distance : Position >< Position -> Real

distance((x₁, y₁),(x₂, y₂)) is

((x₂ – x₁)**2.0 + (y₂ – y₁)**2.0)**0.5

end

Здесь тип Position предназначен для описания координат точек на плоскости, константа origin задает начало координат, функция distance определяет способ вычисления расстояния между двумя точками. Обратите внимание на то, что при описании константы origin и функции distance использован явный стиль описания, т.к. указано непосредственное значение константы и формула для вычисления расстояния.

Дополнить заданную спецификацию определением:

1. типа Circle для описания окружности по ее центру и радиусу;

2. функции on_circle, определяющей, лежит ли точка с заданными координатами на заданной окружности;

3. окружности с радиусом 3.0 и центром в начале координат;

4. константы pos для представления произвольной точки, лежащей на заданной окружности.

Указания:

• в пункте (a) определите вспомогательные типы Center и Radius для представления центра окружности и ее радиуса соответственно, для определения типа Center используйте тип Position, для типа Radius воспользуйтесь следующим описанием:

Radius = { r : Real :- r >= 0.0 },

задающим подтип действительных чисел с неотрицательными значениями;

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

• в пункте (d) используйте неявный стиль описания константы.

1. Для обеспечения работы с рациональными числами предложить спецификацию схемы RATIONAL_NUMBERS, содержащей определения:

1. типа Rational для представления рациональных чисел;

2. функции less, которая сравнивает два рациональных числа и возвращает true, если первое число меньше второго;

3. функции add для сложения двух рациональных чисел;

4. функции max для определения максимума из двух рациональных чисел;

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

Указания: используйте явный стиль спецификации.

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

[approx_sqrt(x,eps), approx_sqrt(x,eps) + eps).