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

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

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

all_natural_numbers : Nat^

axiom

all_natural_numbers(1) = 0,

 idx : Nat •

idx  2

all_natural_numbers(idx) = all_natural_numbers(idx 1)  1

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

n  n in all_natural_numbers • is_a_prime(n)

1. Операции над списками

Над списками в RSL определены следующие операции:

^ : T^*  T^  T^

hd : T^  T

tl : T^  T^

len : T^  Nat

elems : T^  T-infset

inds : T^  Nat-infset

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

Результатом применения операций hd и tl являются соответственно головной элемент списка и оставшаяся после удаления головного элемента часть списка, причем обе эти операции определены только для непустого списка.

Операция len возвращает длину конечного списка, при применении к бесконечному списку результатом является chaos.

Операция elems выдает в качестве результата множество, состоящее из элементов заданного списка. Например, количество различных элементов списка L можно определить с помощью выражения card elems L.

Результатом применения операции inds является множество индексов заданного списка. Таким образом, для конечного списка fl:

inds fl = {1 .. len fl},

для бесконечного списка il:

inds il = {idx  idx : Nat • idx  1}.

Упражнения

1. Определить следующие функции:

1. ‘length’ – вычисляет длину списка без использования встроенной операции len,

2. ‘rev’ – переставляет элементы списка в обратном порядке.

Указания:

• используйте рекурсивное определение функций с помощью операций hd и tl;

• в рекурсивном определении воспользуйтесь условным выражением или конструкцией case.

1. Определить функцию ‘pascal’, генерирующую треугольники Паскаля до порядка n включительно. Результатом функции является список из n списков, каждый из которых задает очередной ряд треугольника. Например, для n = 5 получим список:

1

1 , 1

1 , 2 , 1

1 , 3 , 3 , 1

1 , 4 , 6 , 4 , 1

Очередной k-ый ряд треугольника (k1) начинается и заканчивается 1, i‑ый элемент ряда (1ik) вычисляется как сумма (i1)-го и i-го элементов (k‑1)-го ряда.

Указания:

• определите тип N1 для описания элементов очередного ряда треугольника;

• используйте рекурсивное определение функции через операцию ^;

• в рекурсивном определении воспользуйтесь сокращенным выражением для конструирования списка.

1. Предложить спецификацию следующей упрощенной модели системы обработки текстов: текст разделен на страницы, каждая страница состоит из строк каких-то слов. Определить модуль ‘PAGE’, обеспечивающий описание:

1. типов ‘Page’, ’Line’, и ’Word’ для описания соответственно страницы, строки и слова текста,

2. функции ‘is_on’, проверяющей, встречается ли указанное слово на заданной странице,

3. функции ‘number_of’, подсчитывающей количество вхождений указанного слова в текст заданной страницы.

Указания:

• в пункте (a) воспользуйтесь конечными списками для описания типов ‘Page’ и ’Line’,

• в пункте (b) используйте квантифицированное выражение и операции inds и elems,

• в пункте (c) опишите с помощью сокращенного выражения множество пар индексов (номер строки, номер слова в строке), определяющее все вхождения указанного слова в строки данной страницы, и воспользуйтесь операцией card.

1. Отображения (maps)

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

1. Понятие отображения

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

[3 ↦ true, 5 ↦ false]

[Klaus ↦ 7, John ↦ 2, Mary ↦ 7]

Первый пример задает отображение из натуральных чисел в значения типа Bool, второй – из типа Text в тип Nat. Областью определения (доменом) для первого отображения является множество {3,5}, областью его значений – множество {true,false}, для второго отображения такими множествами являются {Klaus,John,Mary} и {2,7}.

Тип отображения задается следующей конструкцией:

type_expr₁ m type_expr₂

Отображение может быть конечным или бесконечным в зависимости от того, конечным или бесконечным является набор пар, определяющий это отображение. Конечное отображение имеет вид:

[v₁ ↦ w₁,…,v_n ↦ w_n],

бесконечное отображение имеет вид:

[v₁ ↦ w₁,…,v_n ↦ w_n,…],

где n  0, v_i и w_i – некоторые выражения типа type_expr₁ и type_expr₂ соответственно.

Отображение может быть детерминированным или недетерминированным при применении к элементам из его домена. Для детерминированного отображения справедливо соотношение:

v_i  v_j  w_i  w_j ,

где v_i и v_j – любые элементы из домена этого отображения.

Примером конечного детерминированного отображения может служить любое из приведенных выше отображений, имеющих тип Nat m Bool и Text m Nat соответственно. В качестве примера конечного недетерминированного отображения можно привести отображение:

[3 ↦ true,3 ↦ false],

имеющее тип Nat m Bool.

1. Способы определения отображений

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

[v₁ ↦ w₁,…,v_n ↦ w_n],

где n  0. В частности, при n  0 имеем пустое отображение []. Именно этот способ был использован во всех рассмотренных ранее примерах. Порядок следования пар в отображении несущественен, поэтому, например, следующие два выражения задают одно и то же отображение:

[3 ↦ true,5 ↦ false]  [5 ↦ false,3 ↦ true]

(для отображений определены отношения  и ).

Сокращенное выражение (comprehended map expression) используется для определения значений как конечных, так и бесконечных отображений и имеет вид:

[ value_expr_pair  set_limitation ],

где value_expr_pair задает общую формулу для определения входящих в отображение пар, set_limitation задает возможные ограничения на область определения (домен) отображения. Например, значением сокращенного выражения:

[ n ↦ 2n  n : Nat • n  2 ]

является конечное отображение [0 ↦ 0,1 ↦ 2,2 ↦ 4].

Выражение [ n ↦ 2n  n : Nat ] определяет бесконечное отображение [0 ↦ 0,1 ↦ 2,2 ↦ 4,…].

Значение отображения для какого-либо конкретного элемента из его домена задается с помощью выражения  value_expr₁(value_expr₂),  где  value_expr₁ является выражением, определяющим данное отображение, value_expr₂ – выражение для вычисления значения некоторого элемента из домена отображения. Например:

[Klaus ↦ 7, John ↦ 2, Mary ↦ 7](John)  2,

[1 ↦ [Per ↦ 5, Jan ↦ 7], 2 ↦ []](1)(Jan) 

 [Per ↦ 5, Jan ↦ 7] (Jan)  7,

или для недетерминированного отображения:

[3 ↦ true,3 ↦ false](3)  true ^ false,

где символ ^ означает недетерминированный выбор из двух указанных значений.

1. Операции над отображениями

Над отображениями определены следующие операции:

dom : (T₁ m T₂)  T₁-infset

rng : (T₁ m T₂)  T₂-infset

† : (T₁ m T₂)  (T₁ m T₂)  (T₁ m T₂)

∪ : (T₁ m T₂)  (T₁ m T₂)  (T₁ m T₂)

\ : (T₁ m T₂)  T₁-infset  (T₁ m T₂)

/ : (T₁ m T₂)  T₁-infset  (T₁ m T₂)

 : (T₂ m T₃)  (T₁ m T₂)  (T₁ m T₃)

Результатом операции dom является домен отображения, причем в зависимости от вида отображения это множество может быть конечным или бесконечным. Например:

dom [3 ↦ true, 5 ↦ false, 5 ↦ true]  {3,5}

dom []  {}

dom [ n ↦ 2n  n : Nat ]  { n  n : Nat }

Операция rng возвращает в качестве результата область значений отображения.

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

[3 ↦ true, 5 ↦ false] † [5 ↦ true]  [3 ↦ true, 5 ↦ true]

[3 ↦ true] † [5 ↦ false]  [3 ↦ true, 5 ↦ false]

[3 ↦ true] † []  [3 ↦ true]

Операция ∪ просто объединяет наборы пар двух заданных отображений, например:

[3 ↦ true, 5 ↦ false] ∪ [5 ↦ true]  [3 ↦ true, 5 ↦ false, 5 ↦ true]

Операции \ и / позволяют изменять область определения отображений, а именно: \ удаляет из домена отображения указанное множество, / , наоборот, оставляет в домене только те элементы, которые входят в указанное множество. Более точно определение этих операций выглядит следующим образом:

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

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