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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

if a then expr₁ else expr₂ end 

if a then expr₁[true/a] else expr₂[false/a ] end (3)

if chaos then expr₁ else expr₂ end  chaos (4)

Запись вида expr₁[true/a] обозначает подстановку в выражение expr₁ значения true вместо a.

Квантифицированные выражения языка RSL имеют традиционную форму и используются в основном для записи аксиом. Допускаются кванторы: , , .

Упражнения

1. Ниже приведены равенства, которые верны в классической логике. Какие из них верны в RSL?

1. (a)  a

2. true  a  true

3. a  true  true

4. a  true  true

5. a  b  a  b

6. a  a  true

7. (a  a)  false

8. (a  b)  c  a  (b  c)

9. (a  b)  c  a  (b  c)

10. (a  a)  true

11. (a  a)  true

Указания:

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

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

Например, для пункта (c):

chaos  true  chaos,

(chaos  true)  false

Следовательно, утверждение (c) неверно в RSL.

1. Упростить следующие выражения:

1. if true then false else chaos end  ?

2. if a then ( a  chaos) else false end  ?

Указание: воспользуйтесь свойствами (1) - (4) раздела 1.1.2.

1. Какие из следующих выражений верны ?

1.  i : Int •  j : Int • i+j  0

2.  i : Int •  j : Nat • i+j  0

3.  i : Int •  j : Int • i+j  0

1. Напишите RSL выражение, выражающее тот факт, что нет наибольшего целого числа.

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

1. Завершите определение функции, которая проверяет, является ли ее аргумент четным числом.

is_even : Nat  Bool

is_even(n)  ...

Указания:

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

1. Описание функций

Цель данного раздела - познакомить читателя с различными принятыми в RSL стилями описания констант и функций, а также дать методические рекомендации по выбору того или иного стиля описания в зависимости от решаемой задачи. Раздел содержит упражнения по выработке навыков описания констант и функций языка RSL в явном (explicit), неявном (implicit) и аксиоматическом (axiomatic) стилях.

1. Декартовы произведения ( products )

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

(1,2)

(1,true,John).

В декартовом произведении существенен порядок следования элементов, т.е. (1,2) и (2,1) являются различными значениями.

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

type_expr₁  ...  type_expr_n, где n2.

Значениями такого типа являются декартовы произведения длины n (v₁,...,v_n), где каждое v_i – некоторое значение типа type_expr_i.

Примеры записи значений декартовых произведений с указанием их типов:

(true,p  q) : Bool  Bool

(x + 1, 0, this is a text) : Nat  Nat  Text

Над декартовыми произведениями разрешены операции = и .

1. Описание констант

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

Описание констант (value definition) в языке RSL может производиться в одном из трех стилей:

• явном (explicit),

• неявном (implicit),

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

Явный стиль описания применяется, когда непосредственно указывается значение константы. Например, RSL- спецификация вида:

value x : Int = 1

определяет целочисленную константу x=1.

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

value x : Int • x > 0

определяет целочисленную константу x, значением которой может являться любое целое положительное число. Спецификация при этом получается неполной и может быть уточнена в дальнейшем. Такой прием называется недоспецификацией (under-specification) и применяется в том случае, когда описываемое значение по каким-либо причинам не может быть определено полностью.

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

value x : Int

axiom x  1 (для явного описания),

value x : Int

axiom x > 0 (для неявного описания).

1. Описание функций

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

1. Всюду вычислимые и частично вычислимые функции

Функция f, отображающая значения типа T₁ в значения типа T₂, является всюду вычислимой (total function), если для любого значения из T₁ f возвращает некоторое единственное значение из T₂, т.е. f обладает следующим свойством:

 x : T₁ • ! y : T₂ • f(x)  y

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

f : T₁  T₂

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

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

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

f : T₁  T₂

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

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

1. Явный стиль описания функций

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

value

f : Int  Int

f(x)  x + 1

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

value

p : Real  Real

p(x)  1.0/x

pre x  0.0

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

1. Неявный стиль описания функций

Описание функции в неявном стиле (implicit function definition), абстрагируясь от конкретного алгоритма, во главу угла ставит формализацию отношений, связывающих между собой входные и выходные параметры, т.е. здесь описывается не сам алгоритм, а эффект его применения. Этот стиль описания является более общим в том смысле, что алгоритм преобразования не уточняется и, следовательно, для одной и той же неявной спецификации можно предложить разные алгоритмы, эффект применения которых удовлетворяет указанной спецификации. Ниже приведены примеры описания в неявном стиле всюду вычислимой функции 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

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

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

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

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

value

f : Int  Int

axiom  x : Int • f(x)  x + 1

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

value

square_root : Real  Real

axiom

 x : Real • x  0.0 

 s : Real •

square_root(x) = s /\

s  s = x /\ s  0.0

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

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

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

1. выбрать тип:

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

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

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

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

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

1. выбрать стиль описания:

1. явный (можно задать формулу вычисления результата),

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

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

Упражнения

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

2. Пусть система координат описывается следующим образом:

Характеристики

Список файлов книги