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

Например:dom [3 ↦ true, 5 ↦ false, 5 ↦ true] = {3,5}dom [] = {}dom [ n ↦ 2∗n | n : Nat ] = { n | n : Nat }23Операция rng возвращает в качестве результата область значенийотображения.Результатом операции † является набор пар, полученный объединениемнаборов пар первого и второго отображений, причем в случае пересеченияобластей определения предпочтение отдается парам из второго отображения, т.е.для элементов, попавших в пересечение доменов отображений, второеотображение перекрывает первое. Эффект выполнения данной операциииллюстрируют следующие примеры:[3 ↦ true, 5 ↦ false] † [5 ↦ true] = [3 ↦ true, 5 ↦ true][3 ↦ true] † [5 ↦ false] = [3 ↦ true, 5 ↦ false][3 ↦ true] † [] = [3 ↦ true]Операциянапример:∪ просто объединяет наборы пар двух заданных отображений,[3 ↦ true, 5 ↦ false] ∪ [5 ↦ true] = [3 ↦ true, 5 ↦ false, 5 ↦ true]Операции \ и / позволяютотображений, а именно: \ удаляетизменятьиз доменаобластьопределенияотображения указанноемножество, / , наоборот, оставляет в домене только те элементы, которыевходят в указанное множество.

Более точно определение этих операцийвыглядит следующим образом:m \ s = [d ↦ m(d) | d : T1 • d ∈ dom m ∧ d ∉ s]m / s = [d ↦ m(d) | d : T1 • d ∈ dom m ∧ d ∈ s]Некоторые примеры:[3 ↦ true, 5 ↦ false] \ {5,7} = [3 ↦ true][3 ↦ true, 5 ↦ false] / {5,7} = [5 ↦ false][3 ↦ true, 5 ↦ false] \ {3,5,7} = [][3 ↦ true, 5 ↦ false] / {3,5,7} = [3 ↦ true, 5 ↦ false]Операция ° позволяет осуществлять композицию двух отображений, т.е.для отображений m1 и m2 она определяется так:m1 ° m2 = [x ↦ m1(m2(x)) | x : T1 • x ∈ dom m2 ∧ m2(x) ∈ dom m1]Например:[3 ↦ true, 5 ↦ false] ° [″Klaus″ ↦ 3, ″John″ ↦ 7] = [″Klaus″ ↦ true][3 ↦ true] ° [″Klaus″ ↦ 5] = []24Упражнения1. Пусть база данных университета описана следующим образом (для простотыкомментарии приведены на русском языке):schemeMAP_UNIVERSITY_SYSTEM =classtypeStudent,Course,CourseInfos = Course −m→ Student-set,University = Student-set × CourseInfosvalue/∗ allStudents возвращает множество всех студентов, обучающихсяв данном университете ∗/allStudents : University → Student-set,/∗ hasCourse проверяет, читается ли данный курс в данномуниверситете∗/hasCourse : Course × University → Bool,/∗ numberOK возвращает значение true, если любой читаемый вуниверситете курс посещает не менее 5 и не более 100 студентов ∗/numberOK : University → Bool,/∗ studOf возвращает множество студентов заданного университета,посещающих заданный курс ∗/studOf : Course × University −∼→ Student-set,/∗ attending возвращает множество курсов, которые посещаетзаданный студент в указанном университете ∗/attending : Student × University −∼→ Course-set,/∗ newStud добавляет нового студента к числу студентов заданногоуниверситета ∗/newStud : Student × University −∼→ University,/∗ dropStud исключает указанного студента из числа студентовзаданного университета ∗/dropStud : Student × University −∼→ UniversityendОпределите функции, сигнатура которых приведена в данном описании.Указания: воспользуйтесь явным стилем описания функций и операцияминад отображениями.25Глава 2.

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

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

Генеалогическое дерево.Система поддержки генеалогического дерева должна предоставлятьследующие возможности: добавлять в дерево нового члена семьи (ребенка,супруга, предка), вносить изменения в узлы дерева (например, фиксироватьсмену фамилии или дату смерти), осуществлять поиск полезной информациипо дереву (например, для указанного члена семьи находить его детей инаоборот).3. Железнодорожное расписание станции.На железнодорожной станции имеется набор платформ и путей, на которыемогут прибывать поезда, известны номера прибывающих поездов, время ихприбытия и отправления, а также станции отправления и назначения.Система поддержки железнодорожного расписания станции должна26обеспечивать возможность формирования расписания, внесения в негоизменений и выдачу полезной информации (например, список поездов доуказанной станции назначения).4.

Управление семафорами и стрелками на участке железной дороги.Задан участок железной дороги, конфигурация которого приведена ниже. Вузлах участка установлены семафоры и стрелки, состояния которыхопределяют движение поезда по той или иной ветке участка. Считается, чтона каждой ветке может находиться не более одного поезда и все поезда научастке движутся в одном направлении слева направо. Система поддержкиуправления семафорами и стрелками должна обеспечивать следующиеоперации: открыть/закрыть семафор, повернуть стрелку налево/направо (приэтом необходимо учитывать текущее положение стрелки и конфигурациюучастка железной дороги), а также обеспечивать выдачу полезнойинформации (например, о наличии в данный момент поезда на ветке).5.

Система поддержки составления расписания занятий.Система должна обеспечивать возможность составления расписаниянекоторого учебного заведения, внесения в расписание изменений и выдачуполезной информации (например, по итоговому расписанию получитьрасписание указанной группы на заданный день). В расписании должныфиксироваться время и место проведения занятия, предмет и преподаватель,проводящий занятие, а также номер группы, для которой это занятиепроводится. Расписание не должно содержать коллизий (например, разныезанятия не должны пересекаться друг с другом по месту и времени ихпроведения).6.

Планирование автобусного движения в районе.В районе имеется несколько автовокзалов, у каждого из которых есть рядпосадочных площадок. Между автовокзалами курсируют рейсовые автобусы,для каждого рейса фиксируется станция отправления и назначения,посадочная площадка, с которой происходит отправление, а также времяпосадки в автобус и время в пути. Система поддержки планированияавтобусного движения должна обеспечивать возможность добавлять/удалятьновые рейсы, вносить изменения в уже имеющиеся рейсы и выдаватьполезную справочную информацию (например, для указанного автовокзалаопределять все рейсы, отправляющиеся с заданной посадочной площадки ит.д.).277. Заказ/учет товаров в ″бакалейной лавке″.В ″бакалейной лавке″ для каждого товара фиксируется место хранения(определенная полка), количество и поставщик этого товара. Системаподдержки заказа/учета товаров должна обеспечивать возможностьдобавления/удаления нового товара, изменения информации об имеющемсятоваре (например, при изменении количества товара и т.д.) и выдачинеобходимой справочной информации (например, список товаров,количество которых необходимо пополнить).8.

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

При выделении областипамяти по запросу процесса, процесс становится владельцем данной области.Различные процессы могут получать доступ к памяти на чтение и запись.Определение и изменение прав доступа осуществляется только владельцем.Неявная и алгебраическая спецификация должны описывать широкийспектр стратегий управления памятью.10. Информационное табло по состоянию авиарейсов.На табло отражается следующая информация о рейсе: номер рейса, пунктвылета, время прилета по расписанию, ожидаемое время прилета, статус(отложен, вылетел, прилетел). Система поддержки информационного таблодолжна обеспечивать добавление и удаление информации о рейсах, а такжевнесение изменений в состояние табло, если произошло некоторое событие(например, вылет какого-то рейса отложен на N минут, произошла посадкасамолета указанного рейса и т.д.)11. Управление версиями программного проекта.Программный проект представляет собой некоторую совокупность программ,каждая программа в свою очередь состоит из файлов, файлы связаны друг сдругом отношением ″использует″.

Для каждого файла может существоватьнесколько его вариантов и для каждой программы соответственно несколькоее версий. Конкретный вариант файла однозначно идентифицируется именемфайла и номером варианта, аналогично версия программы идентифицируетсяименем программы, номером версии и списком вариантов файлов. Каждаяверсия программы должна быть замкнута по отношению ″использует″.28Система поддержки управления версиями должна обеспечивать возможностьсоздавать новые варианты файлов и новые версии программ, добавлять иисключать варианты файлов из версий без нарушения указаннойзамкнутости, т.е.

нельзя, например, удалить из версии какой-то вариантфайла, если он используется оставшимися файлами.12. Система поддержки составления расписания поездов на железной дороге.Железная дорога представляет собой сеть станций, связанных между собойпутями, (причем могут существовать как однопутные, так и двухпутныеперегоны), на каждой станции имеется N путей, для каждого перегонаизвестно время, необходимое для его прохождения. В расписанииуказывается список поездов данной железной дороги с указанием маршрутових следования (маршрут следования задается списком станций, на которыхостанавливается поезд) и временем прибытия/отправления на станциимаршрута. Расписание должно быть свободно от коллизий, т.е. на путиперегона так же, как и на пути станции не может находиться одновременноболее одного поезда.

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