Е.А. Кузьменкова - Формальная спецификация программ (1184224), страница 4
Текст из файла (страница 4)
Этотспособприменяется в том случае, когда новый список строится на основе какого-то ужесуществующего. Здесь value_expr определяет общую формулу длявычисления значений элементов нового списка, list_limitation задает базовыйсписок, на основе которого строится данный, с возможным указаниемнекоторого предиката для отбора элементов из базового списка.Например, в выражении:〈2∗n | n in 〈0 .. 3〉〉базовым является список 〈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Значение бесконечного списка может быть задано с помощью аксиом,определяющих правила формирования списка. Так, список, содержащий всенатуральные числа в возрастающем порядке, может быть определен следующимобразом:valueall_natural_numbers : Natωaxiomall_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)〉191.4.3. Операции над спискамиНад списками в RSL определены следующие операции:^ : T* × T ω → T ωhd : Tω −∼→ Ttl : Tω −∼→ Tωlen : Tω −∼→ Natelems : Tω → T-infsetinds : 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. Определить следующие функции:(a) ‘length’ – вычисляет длину списка без использования встроеннойоперации len,(b) ‘rev’ – переставляет элементы списка в обратном порядке.Указания:• используйте рекурсивное определение функций с помощью операцийhd и tl;• в рекурсивном определении воспользуйтесь условным выражением иликонструкцией case.2.Определить функцию ‘pascal’, генерирующую треугольники Паскаля допорядка n включительно. Результатом функции является список из nсписков, каждый из которых задает очередной ряд треугольника. Например,для n = 5 получим список:〈1〉〈1 , 1〉〈1 , 2 , 1〉〈1 , 3 , 3 , 1〉〈1 , 4 , 6 , 4 , 1〉20Очередной k-ый ряд треугольника (k>1) начинается и заканчивается 1, i-ыйэлемент ряда (1<i<k) вычисляется как сумма (i−1)-го и i-го элементов (k-1)-горяда.Указания:• определите тип N1 для описания элементов очередного рядатреугольника;• используйте рекурсивное определение функции через операцию ^;• в рекурсивном определении воспользуйтесь сокращенным выражениемдля конструирования списка.3.Предложить спецификацию следующей упрощенной модели системыобработки текстов: текст разделен на страницы, каждая страница состоит изстрок каких-то слов.
Определить модуль ‘PAGE’, обеспечивающийописание:(a) типов ‘Page’, ’Line’, и ’Word’ для описания соответственностраницы, строки и слова текста,(b) функции ‘is_on’, проверяющей, встречается ли указанное слово назаданной странице,(c) функции ‘number_of’, подсчитывающейколичествовхожденийуказанного слова в текст заданной страницы.Указания:• в пункте (a) воспользуйтесь конечными списками для описания типов‘Page’ и ’Line’,• в пункте (b) используйте квантифицированное выражение и операцииinds и elems,• в пункте (c) опишите с помощью сокращенного выражения множествопар индексов (номер строки, номер слова в строке), определяющее всевхождения указанного слова в строки данной страницы, ивоспользуйтесь операцией card.1.5.Отображения (maps)Цель данного раздела - познакомить читателя с понятием отображения(map), принятыми в RSL способами описания отображений и основнымиоперациями над ними.
Раздел содержит упражнения по использованиюабстракции отображений в спецификациях.1.5.1. Понятие отображенияОтображением называется неупорядоченный набор пар значений, которыйотображает значения одного типа в значения другого типа, при этом множествоотображаемых значений называется областью определения или доменом(domain) отображения, а множество значений, в которые осуществляетсяотображение, называется его областью значений (range). Например:[3 ↦ true, 5 ↦ false]21[″Klaus″ ↦ 7, ″John″ ↦ 2, ″Mary″ ↦ 7]Первый пример задает отображение из натуральных чисел в значения типа Bool,второй – из типа Text в тип Nat. Областью определения (доменом) дляпервого отображения является множество {3,5}, областью его значений –множество {true,false}, для второго отображения такими множествамиявляются {″Klaus″,″John″,″Mary″} и {2,7}.Тип отображения задается следующей конструкцией:type_expr1 −m→ type_expr2Отображение может быть конечным или бесконечным в зависимости оттого, конечным или бесконечным является набор пар, определяющий этоотображение.
Конечное отображение имеет вид:[v1 ↦ w1,…,vn ↦ wn],бесконечное отображение имеет вид:[v1 ↦ w1,…,vn ↦ wn,…],где n ≥ 0, vi и wi – некоторые выражения типа type_expr1 и type_expr2соответственно.Отображение может быть детерминированным или недетерминированнымпри применении к элементам из его домена. Для детерминированногоотображения справедливо соотношение:v i = v j ⇒ wi = wj ,где vi и vj – любые элементы из домена этого отображения.Примером конечного детерминированного отображения может служитьлюбое из приведенных выше отображений, имеющих тип Nat −m→ Bool иText −m→ Nat соответственно.Вкачествепримераконечногонедетерминированного отображения можно привести отображение:[3 ↦ true,3 ↦ false],имеющее тип Nat −m→ Bool.1.5.2. Способы определения отображенийДля определения отображений в RSL используются те же способы, что идля множеств и списков, а именно: явное перечисление элементов исокращенное выражение.
Первый способ применяется для конечныхотображений, в этом случае отображение задается выражением вида:[v1 ↦ w1,…,vn ↦ wn],где n ≥ 0. В частности, при n = 0 имеем пустое отображение []. Именно этотспособ был использован во всех рассмотренных ранее примерах. Порядокследования пар в отображении несущественен, поэтому, например, следующиедва выражения задают одно и то же отображение:[3 ↦ true,5 ↦ false] = [5 ↦ false,3 ↦ true](для отображений определены отношения = и ≠).22Сокращенное выражение (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_expr1(value_expr2), где value_expr1является выражением, определяющим данное отображение, value_expr2 –выражение для вычисления значения некоторого элемента из доменаотображения. Например:[″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.5.3. Операции над отображениямиНад отображениями определены следующие операции:dom : (T1 −m→ T2) → T1-infsetrng : (T1 −m→ T2) → T2-infset† : (T1 −m→ T2) × (T1 −m→ T2) → (T1 −m→ T2)∪ : (T1 −m→ T2) × (T1 −m→ T2) → (T1 −m→ T2)\ : (T1 −m→ T2) × T1-infset → (T1 −m→ T2)/ : (T1 −m→ T2) × T1-infset → (T1 −m→ T2)° : (T2 −m→ T3) × (T1 −m→ T2) → (T1 −m→ T3)Результатом операции dom является домен отображения, причем взависимости от вида отображения это множество может быть конечным илибесконечным.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
