Евгений Корныхин - Формальная спецификация программ (Евгений Корныхин - Формальная спецификация программ.pdf), страница 5

[1 ↦→ 1, 4 ↦→ 2, 9 →↦ 3, ...]1.13.4Записать отображение из любого натурального числа в его40Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)простой делитель.1.13.5 Записать отображение любого натурального числа в большееего простое натуральное число. [1 ↦→ 5, 2 ↦→ 7, 3 ↦→ 5, ...]1.13.6Записать отображение «бесконечная перестановка».1.13.7Записать отображение любого натурального числа в своё«зеркало» – число из цифр исходного числа, записанных в обратномпорядке.

[1 ↦→ 1, ..., 12 ↦→ 21, ..., 832 ↦→ 238, ...]1.13.8 Записать отображение любого текста в его реверсию. [..., "стол" ↦→"лотс", "книга" ↦→ "агинк", ...]1.13.9 Не меняя описания предыдущей константы, описать новоеотображение любого текста, начинающегося с ’a’, в его реверсию.1.13.10Записать тип «Англо-русский словарь» так, как Вы егопредставляете. Учтите, что слово может иметь несколько переводов.Схемы сокращения записиЯзык RSL обладает достаточно богатыми возможностями для записи выражений. В данном параграфе предлагается освоить ряд приемовпо получению более краткой записи выражений за счёт использованияразличных предопределенных операций над множествами, списками иотображениями.схема пересечения ∩ { () | : }вместо{ | : ∙ ∈ ∧ (∃ : ∙ = ())}схема вычитания-1 ∖ { () | : }вместо{ | : ∙ ∈ ∧ ∼ (∃ : ∙ = ())}1.5.

Множества, списки, отображения41схема вычитания-2{ () | : } ∖ вместо{ | : ∙ ∈/ ∧ (∃ : ∙ = ())}схема выборки по ключам (на примере) Из исходного отображения выделить подотображение с определенными ключами:/{1, 2}вместо[ ↦→ () | : ∙ ∈ dom ∧ ∈ {1, 2}]схема выборки по значению Из исходного отображения выделитьподотображение с определенными значениями:[1 ↦→ 1, 2 ↦→ 2] ∘ вместо[ ↦→ () | : ∙ ∈ dom ∧ () ∈ {1, 2}]схема соединения (join) Для компактной записи выражений, гденужно «соединение» двух отображений (join), следует использовать композицию отображений (это ее основное практическое применение).ЗадачиЗаписать следующие выраженияПри записи решений стараться выбирать наиболее короткую запись.1.14.1 Дано непустое множество натуральных чисел m и натуральное число x.

Записать логическое выражение, истинное тогда и толькотогда, когда x равен максимальному числу во множестве m.Решение:1x ∈ m ∧ { 0 . . x} ⊇ m42Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)1.14.2 Дано непустое множество целых чисел m и целое число x.Записать логическое выражение, истинное тогда и только тогда, когда xравен максимальному числу во множестве m.1.14.3 Дано непустое множество натуральных чисел m и натуральное число x.

Записать логическое выражение, истинное тогда и толькотогда, когда x равен минимальному числу во множестве m.1.14.4 Дано непустое множество натуральных чисел m. Записатьсумму элементов этого множества.Решение:1card {( x , y ) | x , y : Nat∙x ∈ m ∧ y < x}1.14.5 Дано непустое множество целых чисел m. Записать суммуэлементов этого множества.1.14.6 Дано непустое множество натуральных чисел m.

Записатьпроизведение элементов этого множества.1.14.7 Дан непустой список t, натуральное число x и значение yтого же типа, каков тип элементов в t. Записать логическое выражение, истинное тогда и только тогда, когда x является индексом первоговхождения y в t.1.14.8 Дан непустой список t, натуральное число x и значение yтого же типа, каков тип элементов в t. Записать логическое выражение,истинное тогда и только тогда, когда x является индексом последнеговхождения y в t.1.14.9 Дан непустой список t, натуральные числа x1 и x2 (x2 > x1)и значение y того же типа, каков тип элементов в t.

Записать логическое выражение, истинное тогда и только тогда, когда x1 и x2 являютсяиндексами двух подряд вхождений y в t.1.14.10 «особые фамилии». Дано множество «фамилий» t. Записатьмножество фамилий из t, оканчивающихся на «ов».Решение:1t ∩ { z ̂︀ "ов" | z : Text}1.5. Множества, списки, отображения431.14.11 Даны две строки t1 и t2.

Записать логическое выражение,истинное тогда и только тогда, когда t2 является подстрокой строки t1.1.14.12Дана строка t. Записать выражение, равное реверсу строкиt.1.14.13 Дано отображение m некоторого типа в тот же тип. Записать логическое выражение, истинное тогда и только тогда, когда этоотображение является перестановкой.1.14.14 Дано отображение db строк в целые числа, причем все целые числа разные (например, эти числа - это какие-нибудь хэш-значениястрок). В db добавляется строка t и получается db2 (всё остальное соответствие строк и целых чисел из db сохраняется, добавляется новое безнарушения свойства различия целых чисел).

Записать логическое выражение, определяющее db2.Решение:1db2 \ { t } = db ∧ t ∈ dom db2 ∧ db2 ( t ) ∈/ rng dbОбратите внимание, что сразу два требования (что сохраняются всестроки и сохраняется соответствие строк и целых чисел) записано в первом конъюнкте. Обратите также внимание, что хоть и неизвестно целоечисло, поставленное в соответствие строке t в db2, возможно записатьряд важных свойств отображения db2.1.14.15способом:123Игровое поле игры «крестики-нолики» задано следующимtype C e l l == empty | c r o s s | t o etype Nat3 = { | n : Nat ∙ n ∈ { 1 .

. 3 } | }type F i e l d = ( Nat3 × Nat3 ) → C e l lДано f — значение в типе Field. Записать1) логическое выражение, истинное тогда и только тогда, когда в отображении f есть информация обо всех клетках поля;2) выражение, равное числу пустых клеток.1.14.16 Граф задан отображением вершин во множество инцидентных им вершин:441Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)type V, G = V → V -setТакое представление будет считаться «корректным», если каждая вершина встречается среди первых компонент отображения (при отсутствииинцидентных вершин значение в отображении для такой вершины будетпустым множеством).

Записать логическое выражение, истинное тогда итолько тогда, когда данная переменная g типа G является «корректным»представлением графа.1.14.17 Дано «корректное» представление g графа (см. задачу 14)и список вершин p. Записать логическое выражение, истинное тогда итолько тогда, когда p является путём в графе g.111.14.18 Дано «корректное» представление g графа (см. задачу 14) иего вершина v.

Записать выражение, равное множеству вершин, достижимых из v через не более одну промежуточную вершину.Решение:g ( v ) ∪ ( g∘g ) ( v )чуть более длинный вариант:g ( v ) ∪ ∪ rng ( g/g ( v ) )1.14.19 Дано «корректное» представление g графа (см. задачу 14) иего вершина v. Записать выражение, равное множеству вершин, которыминцидентна v.11.14.20 В таксопарке есть следующая база:type Водитель , Машина , Водители = Водитель → МашинаДана b — база водителей с машинами.1) Дана машина c.

Найти всех водителей машины c.2) Найти множество всех различных машин.3) У таксопарка есть доступ к базе машин:1type Машина , Цвет , Машины = Машина → ЦветДана m — база машин с их цветами. Найти водителей, которыеездят на ’красных’ машинах.1.5.

Множества, списки, отображения45Спецификация алгоритмов со структурами данных4В этих задачах требуется переписать приведенные классические алгоритмы работы со структурами данных на RSL. Следите за тем, чтобыспецификация оставалась «читабельной». Вам пригодится конструкция«неявный let».1.15.1 «Алгоритм Дейкстры». Алгоритм предназначен для решения задачи нахождения кратчайших путей в ориентированном графе снеотрицательными пометками вершин. Длина пути — это сумма пометоквходящих в него дуг. В приведенном псевдокоде ищутся пути от вершины 1, остальные вершины графа пронумерованы числами от 2 до n, V —это множество чисел от 1 до n.

C[i,j] дает пометку дуги из i в j, или ∞,если такой дуги нет. Результат помещается в переменную S.S := {1};for i := 2 to n doD[i] := C[1,i];for i := 1 to n-1 dobeginвыбор из множества V\S такой вершины w,что значение D[w] минимально;добавить w к S;for каждая вершина v из множества V\S doD[v] := min(D[v], D[w]+C[w,v])end1.15.2 «Алгоритм Прима». Алгоритм предназначен для решениязадачи нахождения остовного дерева минимальной стоимости. Остовноедерево содержит все вершины исходного графа, но возможно не все егодуги.

В алгоритме V — это множество вершин (множество чисел от 1 доn). Результат формируется в дереве T.T := пустое дерево;U := {1};while U не равно V dobegin4Алгоритмы взяты из книги [1]46Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)(u,v) --- ребро наименьшей стоимости такое, чтоu принадлежит U и v принадлежит V\U;добавить в T (u,v);добавить в U v;end1.6Эксплицитное и имплицитное описаниефункцийРассмотренный ранее способ описания операций (в виде псевдокода) был эксплицитным (explicit, явным) способом описания, посколькув нем было указано явно «алгоритм» вычисления или было дано явное определение функции.

Однако, это не единственный способ описанияфункций в языке RSL.Эксплицитным назовем следующий способ описания функций:1value∼funcname : T1 × . . . × T2 → T3 × . . . × T4funcname ( t1 , . . . , t2 ) ≡...234Т.е. в эксплицитном способе после сигнатуры идет имя функции сформальными аргументами, далее символ ≡ и затем выражение, чьезначение и есть значение функции.Имплицитным назовем следующий способ описания функции:1value∼2345funcname : T1 × .

. . × T2 → T3 × . . . × T4funcname ( t1 , . . . , t2 ) as ( t3 , . . . , t4 )post...В имплицитном способе после сигнатуры идет имя функции с формальными аргументами, далее слово as, далее формальные имена результатов, далее слово post, после которого идет логическое выражение над именами t1, ..., t2, t3, ..., t4. Т.е. в имплицитном способе описаниязадается предикат (набор функциональных свойств результата функции), а не «алгоритм вычисления».Например:1.6. Эксплицитное и имплицитное описание функций147valuemax : Natmax( a , b )postm∨23456× Nat → Natas m= a ∧ a > bm= b ∧ a ≤ bВыражение после слова post будем называть поствыражением.