Евгений Корныхин - Формальная спецификация программ (1185143), страница 3
Текст из файла (страница 3)
. n ⟩ dosum := sum + iend ;variable sum : Natvalue∼sumN : Nat → write sum UnitsumN( n ) ≡sum := 0 ; i := 0 ;doi := i + 1 ;sum := sum + iuntil i = n end ;Способов прервать цикл типа break в RSL нет.Локальные переменные:1.4. Императивное описание операций12345678910111219variable a : Nat , b : Natvalue∼e u c l i d : Unit → read a , b Nateuclid () ≡l o c a l variable a1 : Nat := a ,b1 : Nat := b inwhile a1 > 0 ∧ b1 > 0 doi f a1 > b1 then a1 := a1 − b1e l s e b1 := b1 − a1 endend ;i f a1 = 0 then b1 e l s e a1 endendМассивы-значенияВ отличие от массивов в императивных языках программирования,понимаемых как непрерывная область памяти однотипных элементов, вRSL массивы ближе к спискам в функциональных языках программирования. Массивы в RSL — это значения, у которых нет возможностиизменить отдельный элемент (можно только заменить всё значение массива целиком).
Далее эта особенность будет пояснена на примерах.Следующая функция использует массив целых чисел:∼1value s o r t : Int * → Int *Обращение по индексу делается так: A(1). Нумерация индексов сединицы. Операция len возвращает текущую длину массива. Массивыв RSL могут изменять длину (путем операции конкатенации). Индекс недолжен иметь большее значение, чем длина массива, и меньшее, чем 1.Синтаксис RSL запрещает изменять значения отдельных элементов массивов (например, так: «A(i) := i»), можно только строить новые массивыцеликом (например, вместо «A(i) := e» можно писать «A := ⟨ if k=i thene else A(k) end | k in ⟨1 .. len A⟩ ⟩»).1234value∼sum : Int * → Intsum ( l s ) ≡l o c a l variable s : Int := 0 in2056789Глава 1.
RAISE SPECIFICATION LANGUAGE (RSL)for i in ⟨ 1 . . len l s ⟩ dos := s + l s ( i )end ;send ;Эту же функцию, суммирующую элементы массива, можно записатьи без использования индексов:123456789value∼sum : Int * → Intsum ( l s ) ≡l o c a l variable s : Int := 0 infor l in l s dos := s + lend ;send ;Тип Text является массивом из Char.Операция tl возвращает «подмассив» — от второго элемента до последнего элемента исходного массива. Операция определена только длянепустых массивов.
Пустой массив обозначается символом <..>. Тем самым функцию sum можно записать следующим образом с использованием рекурсии:12345value∼sum : Int * → Intsum ( l s ) ≡i f l s = ⟨ ⟩ then 0e l s e l s ( 1 ) + sum ( t l l s ) endСтруктуры12345type FIO : :name : Textsurname : Textvalue∼h e l l o : FIO → Text1.4. Императивное описание операций21hello ( fio ) ≡" H e l l o , " ̂︀ name ( f i o ) ̂︀" " ̂︀ surname ( f i o ) ̂︀ " ! "678Обращение к полю делается в виде вызова функции с именем поля.123456type FIO : :name : Textsurname : Textvalue∼new_fio : Text × Text → FIOnew_fio ( n , sn ) ≡ mk_FIO( n , sn )Создание структуры делается с помощью функции с предопределенным именем.
Это имя начинается с «mk_», за которым идет имя типаструктуры. В скобках подряд перечисляются выражения, дающие значения полям новой структуры.Перечисления (enumeration)1234type Color = red | b l u e | white | g r e e nvalue∼from_rus : Color → Boolfrom_rus ( c ) ≡ c = red ∨ c = b l u e ∨ c = whiteУказателиRSL не содержит встроенных механизмов для задания алгоритмов,работающих с указателями и работающих с динамической памятью.ЗадачиПереписать алгоритмы на RSL21.1.12Нахождение минимального элементазадачи взяты из [2]22Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)Minimum()1 min ← [1]2 for ← 2 to length[]3do if min > []4then min ← []5 return min1.1.2Сортировка методом вставокSort()1 for ← 2 to length[]2do key ← []3←−14while > 0 and [] > key5do [ + 1] ← []6←−17[ + 1] ← key1.1.3Быстрая сортировка ХоараQuicksort(, , )1 if < 2then ← Partition(, , )3Quicksort(, , )4Quicksort(, + 1, )Partition(, , )1 ← []2 ←−13 ←+14 while TRUE5do repeat ← − 16until [] 6 7repeat ← + 18until [] > 9if < 10then поменять [] ↔ []11else return 1.4.
Императивное описание операций231.1.4 Использовать следующее представление закрытых хеш-таблиц:123type Key ,ClosedHashElement == empty | o c c u p i e d ( elem : Key ) ,ClosedHash = ClosedHashElement *Hash-Insert(, )1 ←02 repeat ← ℎ(, )3if [] = NIL4then [] ← 5return 6else ← + 17until = 8 error «переполнение хеш-таблицы»Решение:123456789101112131415161718192021variable T: ClosedHashvalue m : Natvalue∼h : Key × Nat → Nat ,∼i n s e r t : Key → write T Natinsert (k) ≡l o c a l variableready : Bool := f a l s e ,i n d e x : Nat := 0 infor i in ⟨ 0 . . m−1⟩ dol e t j = h ( k , i ) ini f ∼ready ∧ T( j ) = empty thenT := ⟨ i f i=j then o c c u p i e d ( k )e l s e T( i ) end | i in ⟨ 1 .
. len T⟩ ⟩ ;i n d e x := j ;ready := trueendendend ;indexend24Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)m задана в виде константы. Для вызываемой функции ℎ добавленасигнатура. Предусловие описывает те ситуации, когда исходная процедура не достигнет оператора error. Если известно, что () ̸= empty, томожно вызывать функцию elem( ()), чтобы получить значение, хранящееся в ’м элементе хеш-таблицы.Приведем условие, при котором функция выполнит то, что от нееожидается, т.е.
действительно добавит ключ в хэш-таблицу (т.е. при еевыполнении будет достигнут оператор «return »):1∃ i : Nat∙i ≥ 0 ∧ i ≤ m ∧ T( h ( k , i ) ) = empty1.1.5 Поиск в закрытой хеш-таблице (использовать представлениехэш-таблицы из предыдущей задачи), привести условие, при которомфункция выполнит то, что от нее ожидаетсяHash-Search(, )1 ←02 repeat ← ℎ(, )3if [] = 4then return 5←+16until [] = NIL или = 7 error «отсутствие искомого элемента»Решить задачи31.2.1 Всё, что от вас требуется — найти сумму всех целых чисел,лежащих между 1 и включительно.1.2.2 У вас есть несколько камней известного веса 1 , ..., . Напишите программу, которая распределит камни в две кучи так, что разность весов этих двух куч будет минимальной.1.2.3 Ваша задача — найти минимальное положительное целое число такое, что произведение цифр числа в точности равняется .3задачи взяты с сайта http://acm.timus.ru/1.4.
Императивное описание операций251.2.4 В одном из островных государств Карибского бассейна всерешения традиционно принимались простым большинством голосов наобщем собрании граждан, которых, к счастью, было не очень много.Одна из местных партий, стремясь прийти к власти как можно более законным путем, смогла добиться некоторой реформы избирательной системы.
Главным аргументом было то, что население острова в последнеевремя значительно возросло, и проведение общих собраний пересталобыть легкой задачей.Суть реформы состояла в следующем: с момента введения ее в действие все избиратели острова делились на K групп (необязательно равных по численности).
Голосование по любому вопросу теперь следовало проводить отдельно в каждой группе, причем считалось, что группавысказывается «за», если «за» голосует более половины людей в этойгруппе, а в противном случае считалось, что группа высказывается «против». После проведения голосования в группах подсчитывалось количество групп, высказавшихся «за» и «против», и вопрос решался положительно в том и только том случае, когда групп, высказавшихся «за»,оказывалось более половины общего количества групп.Эта система вначале была с радостью принята жителями острова.Когда первые восторги рассеялись, очевидны стали, однако, некоторыенедостатки новой системы.
Оказалось, что сторонники партии, предложившей систему, смогли оказать некоторое влияние на формированиегрупп избирателей. Благодаря этому, они получили возможность проводить некоторые решения, не обладая при этом реальным большинствомголосов! Пусть, например, на острове были сформированы три группыизбирателей, численностью в 5, 5 и 7 человек соответственно. Тогда партии достаточно иметь трех сторонников в каждой из первых двух групп,и она сможет провести решение всего шестью голосами «за», вместо девяти, необходимых при общем голосовании.Вам надо написать программу, которая определяет по заданному разбиению избирателей на группы минимальное количество сторонниковпартии, достаточное, при некотором распределении их по группам, дляпринятия любого решения.
Количество групп нечетно.1.2.5 Рассмотрим последовательность чисел , = 0, 1, 2, ..., удовлетворяющих следующим условиям: 0 = 0, 1 = 1, 2 = , 2+1 = + + 1 для каждого = 1, 2, 3, ... .Напишите программу, которая для заданного значения находит26Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)максимальное среди чисел 0 , 1 , ..., .1.2.6 Определение 1. !!...! = ( − )( − 2)...( mod ), если не делится на ; !!...! = ( − )( − 2)..., если делится на (знаков! в обоих случаях штук).Определение 2.
mod — остаток от деления на . Например,10 mod 3 = 1; 3! = 3·2·1; 10!!! = 10·7·4·1.Мы по заданным и смогли вычислить значение выражения изопределения 1. А вам слабо?1.2.7 При подготовке задач жюри олимпиады столкнулось со следующей проблемой: нужно было передавать по электронной почте текстызадач. Как известно, электронная почта ненадёжна, сообщения передаются открытым текстом, и существует опасность, что кто-нибудь их перехватит.
Членам программного комитета вовсе не хотелось, чтобы задачи стали известны участникам раньше начала соревнования, поэтомуони прибегли к методам криптографии. Жюри разработало совершенноновый способ шифрования текста, но он пока не запатентован и поэтому держится в секрете. Впрочем, одну тайну мы вам всё же откроем,новый алгоритм основан на работе с простыми числами и, в частности,использует вычисление -го по счёту простого числа.Несколько членов программного комитета, независимо друг от друга,разработали программы, производящие такие вычисления, но эти программы выдают разные ответы. Каждый уверен, что он написал своюпрограмму правильно, поэтому жюри встало в тупик и не может продолжать свою работу.Вы должны помочь жюри и спасти соревнования.
Напишите программу, вычисляющую -е по счёту простое число, и, самое главное, онадолжна работать правильно!1.2.8 Условие этой задачи очень простое: вам всего лишь надо определить, сколько клеток находится под боем шахматного коня, одинокостоящего на шахматной доске. На всякий случай напомним, что конь ходит буквой «Г» — на две клетки по горизонтали или вертикали в любомнаправлении, и потом на одну клетку в направлении, перпендикулярномпервоначальному.1.2.9 Представим себе бесконечную последовательность цифр, составленную из записанных друг за другом возрастающих степеней де-1.5.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
