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

Множества, списки, отображения27сятки. Вот начало этой последовательности: 110100100010000... Всё, чтонадо — определить, какая цифра находится в такой последовательностина определённом месте.1.2.10 Пусть задана последовательность из целых неотрицательных чисел. Медианой такой последовательности в случае нечетного называется элемент, который будет равноудален от концов последовательности, если ее отсортировать по возрастанию или убыванию (нетрудно сообразить, что этот элемент имеет номер 2+1 в отсортированной последовательности, если номера считать с единицы).

В случае четного медианой называется среднее арифметическое двух элементов, которыеокажутся на местах 2 и 2 + 1, если последовательность отсортировать.Однако исходная последовательность не обязана быть отсортированной.Напишите программу, которая по заданной входной последовательности вычисляет ее медиану.1.5Множества, списки, отображенияБолее мощные алгоритмы требуют более сложных структур данных.RSL содержит (в дополнение к уже рассмотренным массивам, структурам и перечислениям) средства для работы с множествами, списками иотображениями.МножестваМножество – это контейнер элементов одного типа, который обладает свойствами уникальности и неупорядоченности его элементов.

Множества бывают конечными и бесконечными.Типовое выражение для конечного множества: -set. Типовое выражение для бесконечного множества: -infset. Конечноемножество – подтип бесконечного множества.Операции над множествами:=: -infset × -infset → Bool – сравнение на равенство̸=: -infset × -infset → Bool – сравнение на не равенство∪ : -infset × -infset → -infset – объединение пары множеств28Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)∪ : -infset-infset → -infset – объединение множества множеств∩ : -infset × -infset → -infset – пересечение пары множеств∩ : -infset-infset → -infset – пересечение множества множеств∖ : -infset × -infset → -infset – вычитание множеств∈: × -infset → Bool – проверка на принадлежность∈:/ × -infset → Bool – проверка на непринадлежность⊂: -infset × -infset → Bool – проверка вложения⊃: -infset × -infset → Bool – проверка вложения⊆: -infset × -infset → Bool – проверка вложения⊇: -infset × -infset → Bool – проверка вложенияcard : -infset ̃︁→ Nat – количество элементов (chaos для бесконечных множеств)Обратите внимание на отсутствие операции выбора произвольногоэлемента из множества!Только операция card дает целое число от множеств, т.е.

любое целочисленное выражение над множествами будет мощностью некоторогомножества.Конструкторы множеств:(пустое множество) {}(перечисление) {0, 1, 2} - множество, состоящее из трех целых чисел (не натуральных!) - нуля, единицы и двойки.(диапазон) {0..2} - то же, что и {0, 1, 2}; {0..0} ≡ {0}, {1..0} ≡ {}(«сокращенная запись») {_ℎ_| : ∙ }(например, {2 ⋆ | : Nat ∙ < 3}, что эквивалентно {0, 2, 4})1.5. Множества, списки, отображения29СпискиСписок – это контейнер элементов одного типа, который обладаетсвойствами упорядоченности элементов.

Для задания списка надо указать не только сами элементы, но и их порядок. Списки бывают конечными и бесконечными.Типовое выражение для конечного списка: ⋆ . Типовое выражение для бесконечного списка: . Конечный список – подтипбесконечного списка.Операции:=: × → Bool – проверка на равенство̸=: × → Bool – проверка на не равенство(.) : × Int ̃︁→ – взятие элемента по индексу (chaos для индекса, отсутствующего в списке, индексы нумеруются с единицы)∧: ⋆ × → – конкатенация списковhd : ̃︁→ – головной элемент списка (chaos для пустого списка)tl : ̃︁→ – хвостовая часть списка (chaos для пустого списка)len : ̃︁→ Nat – количество элементов списка (chaos для бесконечного списка)elems : → -infset – множество элементов списка (без повторений!)inds : → Nat-infset – множество индексов элементов спискаКонструкторы списков:(пустой список ) ⟨⟩(перечисление) ⟨0, 1, 2⟩ - список, состоящий из трех целых чисел (ненатуральных!) - нуля, единицы и двойки - в порядке увеличения.(диапазон) ⟨0..2⟩ - то же, что и ⟨0, 1, 2⟩; ⟨0..0⟩ ≡⟨0⟩, ⟨1..0⟩ ≡⟨⟩(«сокращенная запись») ⟨_ℎ_|in ∙ ⟩(например, ⟨2 ⋆ |in⟨0..2⟩⟩, что эквивалентно ⟨0, 2, 4⟩)30Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)ОтображенияОтображение – это множество пар элементов, у которого первые компоненты не повторяются. Отображения бывают конечными и бесконечными, детерминированными и недетерминированными (это те, в которыхпервые компоненты всё же могут повторяться в разных парах).Типовое выражение для детерминированного отображения:1 −→ 2Типовое выражение для недетерминированного отображения:1 ]−→ 2Операции:=: (1 −→ 2 ) ×(1 −→ 2 ) → Bool – сравнение отображений наравенство̸=: (1 −→ 2 ) ×(1 −→ 2 ) → Bool – сравнение отображений нане равенство(.) : (1 −→ 2 ) × 1 ̃︁→ 2 – взятие значения по индексу (chaos,если значение по этому индексу не определено)dom : (1 −→ 2 ) → 1 -infset – область определения отображенияrng : (1 −→ 2 ) → 2 -infset – область значения отображения† : (1 −→ 2 ) ×(1 −→ 2 ) → (1 −→ 2 ) – обновление отображения∪ : (1 −→ 2 ) ×(1 −→ 2 ) → (1 ]−→ 2 ) – объединение отображений∖ : (1 −→ 2 ) × 1 -infset → (1 −→ 2 ) – уменьшение отображения/ : (1 −→ 2 ) × 1 -infset → (1 −→ 2 ) – проекция отображения1.5.

Множества, списки, отображения31∘ : (2 −→ 3 ) ×(1 −→ 2 ) → (1 −→ 2 ) – композиция отображенийКонструкторы отображений:(пустое отображение) [](перечисление) [0 ↦→ 1, 1 ↦→ 2] – отображение, состоящий из двухпар целых чисел (не натуральных!) - из 0 в 1 и из 1 в 2.(«сокращенная запись») [1 _ℎ_ ↦→ 2 _ℎ_| : ∙ ] (например, [ ↦→ + 1| : Nat ∙ < 3], что эквивалентно [0 ↦→ 1, 1 ↦→ 2, 2 ↦→ 3])ЗадачиВычислить выражения с множествами1.3.1{1, 2} = {3, 1}1.3.2{1, 2} = {2, 1}1.3.3{1, 2, 1} = {2, 2, 1}1.3.4{1, 2} ∪ {3, 4}1.3.5{1, 2} ∪ {2, 3}1.3.6{1, 2} ∩ {3, 4}1.3.7{1, 2} ∩ {2, 3}1.3.8{1..30} ∪ {10..

− 10}1.3.9{1..30} ∩ {10.. − 10}1.3.10{1..30} ∪ { | : Int ∙ abs < 11}1.3.11{1..30} ∩ { | : Int ∙ abs < 11}32Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)1.3.12{ + 10 | : Int} = { | : Int}1.3.13{5 * + 2 | : Int} ∩ {3 * − 1 | : Int}1.3.14{5 * + 2 | : Int} ∖ {3 * − 1 | : Int}1.3.15{5 * + 2 | : Int} ⊂ {3 * − 1 | : Int}1.3.16{5 * + 2 | : Int} ⊇ {3 * − 1 | : Int}1.3.17∼ ({1, 2} ⊆ {2, 1, 1})1.3.18card{1..30}1.3.19card{5 * + 2 | : Int ∙ * ∈ {−10..10}}1.3.20card{5 * + 2 | : Int ∙ * ∈ {10.. − 10}}1.3.21card{ * − 2 * | : Int ∙ * ∈ {−10..10}}1.3.22∀ : Nat ∙ ∈ { | : Int}1.3.23∀ : Int ∙ ∈ { | : Nat}Решите уравнения1.4.1{1} ∪ = {}1.4.2{1} ∪ = {1}1.4.3{1} ∪ = {1, 2}1.4.4{1} ∩ = {}1.4.5{1} ∩ = {1}1.4.6{1} ∩ = {1, 2}1.4.7{2, 1} ∖ = {1}1.5.

Множества, списки, отображения1.4.8card = 01.4.9card = 133Какие из следующих выражений истинныеСчитайте, что свободные переменные располагаются под кванторомвсеобщности1.5.1( ∪ ) ∖ = ( ∖ ) ∪ ( ∖ )1.5.2( ∖ ) ∩ = ( ∩ ) ∖ 1.5.3( ∪ ) ∖ ≡( ∖ ) ∪ ( ∖ )1.5.4 ∪ {} = 1.5.5{} ∪ = 1.5.6( ∪ ) ∩ = ( ∩ ) ∪ ( ∩ )1.5.7card Nat < card Int1.5.8card Nat = card Int1.5.9card Nat > card Int1.5.10card Nat ≡ card Int1.5.11card{ | : Nat} ≡ card{ | : Int}Записать на RSL следующие множества1.6.1Пустое множество;1.6.2 Множество чисел 1, 2, 3 (а также множество чисел от 1 до 3);34Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)1.6.3Множество всех чётных чисел;1.6.4 Множество всех чётных чисел, не превышающих 10 (привестив виде перечисления и нескольких различных сокращённых формах);1.6.5Множество всех простых натуральных чисел;1.6.6Множество всех пар взаимнопростых натуральных чисел;1.6.7 Множество всех троек, в каждой из которых есть одинаковыеэлементы;1.6.8 Множество всех степеней двойки, не превышающих 100 (привести в виде перечисления и нескольких сокращённых формах);1.6.9Множество всех IP-адресов класса А (B, C, D, E);1.6.10Множество всех точек плоскости, образующих1) Прямую – биссектрису I и III квадрантов;2) Правую полуплоскость;3) Нижнюю полуплоскость;4) Единичную окружность;5) Единичный круг;6) Единичный квадрат со сторонами, параллельными осям координат.Вычислить выражения со списками1.7.1⟨1⟩ = ⟨1, 1⟩1.7.2⟨1, 2⟩ = ⟨3, 1⟩1.7.3⟨1, 2⟩ = ⟨2, 1⟩1.5.

Множества, списки, отображения1.7.4⟨1, 2, 3⟩(2)1.7.5⟨1⟩(0)1.7.6⟨1⟩(1)1.7.7⟨1, 2⟩ ∧ ⟨3, 4⟩1.7.8⟨1, 2⟩ ∧ ⟨2, 3⟩1.7.9⟨ + 10 | in ⟨1, 2⟩⟩ = ⟨ | in ⟨1⟩⟩1.7.10hd⟨1, 2, 3⟩1.7.11tl⟨1, 2, 3⟩1.7.12len⟨1, 2, 3⟩1.7.13elems⟨1, 2, 3⟩1.7.14inds⟨1, 2, 3⟩1.7.15len⟨1..30⟩1.7.16let = ⟨1, 2, 3⟩ in elems ∩ inds end1.7.17let = ⟨0, 1, 2⟩ in elems ∩ inds end351.7.18 let : Int ∙ (∀ 1 , 2 : Nat ∙ card{1 , 2 } = card{(1 ), (2 )})in end1.7.19 let : Int ∙ (∀ 1 , 2 : Nat ∙ card{1 , 2 } = card{(1 ), (2 )})in elems ∩ inds end1.7.20∀ : ∙ (0) = hd 1.7.21∀ : ∙ (0) ≡ hd 36Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)Решите уравнения1.8.1⟨1⟩ ∧ = ⟨1⟩1.8.2⟨1⟩ ∧ = ⟨1, 2, 3⟩1.8.3⟨1⟩ ∧ = ⟨3, 2, 1⟩1.8.4tl = ⟨1⟩1.8.5hd = 11.8.6 ∧ tl = 1.8.7tl = ⟨hd ⟩1.8.8elems = inds 1.8.9elems tl = elems 1.8.10len = card elems 1.8.11len = card inds 1.8.12len ≡ card inds Записать на RSL следующие выражения1.9.1Пустой список;1.9.2 Список из чисел 1, 2, 3 (попробуйте привести как можно больше различных решений);1.9.3 Список всех простых натуральных чисел в порядке увеличенияих значения;1.9.4 Список всех пар взаимнопростых натуральных чисел в порядкеувеличения их суммы;1.5. Множества, списки, отображения371.9.5 Список номеров групп 5го курса факультета ВМиК МГУ впорядке увеличения номера группы;1.9.6Количество простых чисел от 1 до 10 (тремя различнымиспособами).Упростить выражения1.10.1⟨ | in ⟨card{..}⟩⟩1.10.2⟨ | in ⟨′ ′ , ′ ′ ⟩⟩1.10.3⟨ | in ⟨′ " ′ ⟩⟩1.10.4⟨ | in ⟨⟩⟩Вычислить1.11.1[ ↦→ 1 | : Nat ∙ ∈ {1..3}]1.11.2[ ↦→ | : Nat ∙ ∈ {5..5}]1.11.3[ ↦→ + 1 | : Nat ∙ ∈ {100..90}]1.11.4[ ↦→ | , : Nat ∙ ∖ = 0 ∧ > 2]1.11.5[ ↦→ | , : Nat ∙ ∈ {1..3} ∧ ∈ {1..}]1.11.6[ ↦→ (, ) | , , : Nat ∙ ∈ {1..100} ∧ + = ∧ ∖ = 0]1.11.7[1 ↦→ 2, 2 ↦→ 3, 3 ↦→ 1](3)1.11.8[1 ↦→ 2, 2 ↦→ 3, 3 ↦→ 1](4)1.11.9[«Маша» ↦→ 30, «Света» ↦→ 15, «Маша» ↦→ 30](«Маша»)38Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)1.11.101.11.116] ] (2) (1)[«Маша» ↦→ 30, «Света» ↦→ 15, «Маша» ↦→ 10](«Маша»)[1 ↦→ [1 ↦→ 1, 2 ↦→ 2, 3 ↦→ 3], 2 ↦→ [1 ↦→ 4, 2 ↦→ 5, 3 ↦→1.11.12dom[3 ↦→ 1, 5 ↦→ 0, 2 ↦→ 88]1.11.13rng[3 ↦→ 1, 5 ↦→ 0, 2 ↦→ 88]1.11.14dom[ ↦→ 2 * | : Nat]1.11.15rng[ ↦→ 2 * | : Nat]1.11.16[1 ↦→ 20, 2 ↦→ 30] ∪[1 ↦→ 30, 2 ↦→ 20]1.11.17[1 ↦→ 20, 2 ↦→ 30] †[1 ↦→ 30, 2 ↦→ 20]1.11.18 [«Миша» ↦→ 170, «Слава» ↦→ 200, «Витя» ↦→ 195] ∖{«Миша», «Петя»}1.11.19 [«Миша» ↦→ 170, «Слава» ↦→ 200, «Витя» ↦→ 195] /{«Миша», «Петя»}1.11.20 Пусть Friend = [«Миша» ↦→ «Аня», «Аня» ↦→ «Леша», «Леша» ↦→«Миша»].

Найти Friend ∘ Friend. Какой смысл этого значения ?1.11.21card dom [1 ↦→ 2, 1 ↦→ 3, 2 ↦→ 3]1.11.22dom([10 ↦→ 100, 20 ↦→ 50] †[20 ↦→ 60, 30 ↦→ 90])1.11.23card rng ([1 ↦→ 2] ∘[3 ↦→ 2, 4 ↦→ 1] ∘[1 ↦→ 2, 3 ↦→ 4])Какие из следующих выражений истинныЕсли выражение ложно, привести контрпример и дополнительныеограничения на входящие переменные, чтобы условие стало верным. Считать, что все переменные стоят под кванторами всеобщности.1.12.1dom ( ∪ ) ≡ dom ∪ dom 1.5.

Множества, списки, отображения1.12.2rng ( ∪ ) ≡ rng ∪ rng 1.12.3dom ( † ) ≡ dom † dom 1.12.4rng ( † ) ≡ rng † rng 1.12.5 = ⇒ dom = dom 1.12.6 ̸= ⇒ dom ̸= dom 1.12.7 ̸= ⇒ rng ̸= rng 1.12.8dom(∖ ) ≡ (dom )∖1.12.9dom(/ ) ≡ 1.12.10dom( † ) ≡ dom ∪ 1.12.11( ∪ ) ∪ ≡ ∪( ∪ )1.12.12( † ) † ≡ †( † )1.12.13( ∘ ) ∘ ≡ ∘( ∘ )1.12.14 ∪ ≡ ∪39Записать на RSL следующие константы и определения типов1.13.1 Записать отображение – перестановку первых натуральныхчисел. Считать константой с sort-определением.1.13.2 Записать отображение-«сдвиг» : [1 ↦→ 2, 2 ↦→ 3, ..., ↦→ 1].Считать константой с sort-определением.1.13.3 Записать отображение всех полных квадратов в своё основание.