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

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

базовым является список <.0 .. 3.>, предикат отбора отсутствует и, следовательно, в результате вычисления получается список <.0,2,4,6.>, причем упорядоченность элементов нового списка полностью определяется порядком следования элементов в базовом списке. Примером использования предиката для отбора элементов базового списка может служить выражение:

<.n  n in <.1 .. 100.> :- is_a_prime(n).>,

где предикат is_a_prime(n) позволяет определить, является ли n простым числом. С помощью данного выражения задается список, элементами которого являются все простые числа из диапазона 1 .. 100 в возрастающем порядке, т.е. <.2,3,5,7,...,97.>.

Для доступа к какому-либо конкретному элементу списка в RSL предусмотрено понятие индекса. В качестве индекса используются натуральные числа, причем индексация элементов списка начинается с 1 и для конечных списков заканчивается числом, равным длине списка. Например:

<.2,5,3.> (2)  5

<.<.2,5,3.>, <.3.>.> (1)  <.2,5,3.>

<.<.2,5,3.>, <.3.> .> (1)(2)  <.2,5,3.> (2)  5

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

<.1 .. 50.> (51)  chaos

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

value

all_natural_numbers : Nat-inflist

axiom

all_natural_numbers(1) = 0,

exists idx : Nat :-

idx >= 2 =>

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

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

<.n  n in all_natural_numbers :- is_a_prime(n).>

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

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

^ : T-list >< T-inflist -> T-inflist

hd : T-inflist --> T

tl : T-inflist --> T-inflist

len : T-inflist --> Nat

elems : T-inflist -> T-infset

inds : T-inflist -> Nat-infset

Кроме того к спискам, как и к любому типу в RSL, применимы операции = и ~=.

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

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

hd L is L(1)

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

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

elems <..> = {}

elems <.1,3,1.> = {1, 3}

elems all_natural_numbers = {n | n : Nat}

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

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

inds <..> = {}

inds <.1,3,1.> = {1, 2, 3}

Таким образом, для конечного списка FL:

inds FL = {1 .. len FL},

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

inds IL = {idx  idx : Nat :- idx >= 1}.

Для произвольного списка L верно соотношение:

elems L is {L(x) | x : Nat :- x isin inds L}

Встроенный тип Text представляет собой конечный список из элементов типа Char, т.е. Text = Char-list, следовательно, к значениям этого типа применимы все операции со списками. Например:

“abc”(2) = <.’a’, ‘b’, ‘c’.>(2) = ‘b’

tl “abc” = “bc”

Выражение case

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

case value_expr of

pattern₁ -> value_expr₁,

...

pattern_n -> value_expr_n

end, где n  1.

Здесь выражение value_expr задает селектор выбора, pattern₁,…,pattern_n – шаблоны подстановки, каждый из которых определяет соответствующий вариант значения выражения. При вычислении выражения значение селектора value_expr последовательно (сверху вниз) сопоставляется с указанными шаблонами до первого совпадения. В случае успешного сопоставления с шаблоном pattern_i дальнейшее сопоставление не производится и в качестве результирующего значения всего выражения принимается значения выражения value_expr_i. Если попытка сопоставления для всех шаблонов закончилась неуспешно, имеет место неполная спецификация (недоспецификация).

В RSL определено несколько видов шаблонов, мы ограничимся рассмотрением только трех из них. Простейшими видами шаблонов являются литеральный шаблон (в качестве шаблонов используются литералы RSL) и шаблон универсальной подстановки (_), сопоставление с которым всегда приводит к успешному результату. В силу своей специфики шаблон универсальной подстановки всегда должен располагаться последним в списке шаблонов выражения case. Использование указанных видов шаблонов иллюстрирует пример спецификации функции, вычисляющей числа Фибоначчи.

type Nat1 = {|n : Nat :- n > 0|}

value Fib: Nat1 -> Nat1

Fib(n) is

case n of

1 -> 1,

2 -> 1,

_ -> Fib(n - 2) + Fib(n - 1)

end

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

value reverse : Int-list -> Int-list

reverse(L) is

case L of

<..> -> <..>,

<.i.> ^ Lr-> reverse(Lr) ^ <.i.>

end

Упражнения

1. Вычислить значение выражения:

1. <.n * n | n in <.1..20.> :- n \ 2 = 1.>(7),

2. <.n * n | n in <.1..20.> :- n \ 2 = 1.>(12).

1. Определить список, элементами которого являются:

(a) четные числа в диапазоне от 2 до 16,

(b) все полные квадраты в диапазоне от 1 до 100.

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

1. Определить список, элементами которого являются числа Фибоначчи, не превосходящие 1000.

Указания:

• определите с помощью аксиом список из всех чисел Фибоначчи,

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

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

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

1. Пусть конечный список образован из элементов типа Elem. Определить следующие функции:

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

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

3. del – удаляет из списка все вхождения заданного элемента,

4. number_of – подсчитывает количество вхождений в список заданного элемента.

Указания:

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

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

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

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

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

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

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

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

Указания:

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

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

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

ГЛАВА 5. ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ‑ОРИЕНТИРОВАННЫХ СПЕЦИФИКАЦИЯХ. ОТОБРАЖЕНИЯ

Понятие отображения, конечные детерминированные отображения. Способы определения отображений. Операции над отображениями. Использование абстракции отображений в моделе-ориентированнных спецификациях. Упражнения.

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

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

[3 +> true, 5 +> false]

[Klaus +> 7, John +> 2, Mary +> 7]

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

Каждая пара отображения задается выражением v +> w и определяет отображение ключа v в значение w. Порядок следования пар в отображении несущественен, поэтому, например, выражения [3 +> true,5 +> false] и [5 +> false,3 +> true] определяют одно и то же отображение.

Тип отображения задается типовым выражением:

T₁ –m-> T₂,

где T₁ - тип элементов домена отображения (ключей) и T₂ – тип элементов области значений отображения. Так, приведенные выше отображения имеют типы  Nat ‑m‑>Bool и Text ‑m‑> Nat соответственно.

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

[v₁ +> w₁,…,v_n +> w_n],

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

[v₁ +> w₁,…,v_n +> w_n,…],

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

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

v_i  v_k => w_i  w_k ,

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

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

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

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