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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

m \ s  [d ↦ m(d)  d : T₁ • d  dom m  d  s]

m / s  [d ↦ m(d)  d : T₁ • 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]

Операция  позволяет осуществлять композицию двух отображений, т.е. для отображений m₁ и m₂ она определяется так:

m₁  m₂  [x ↦ m₁(m₂(x))  x : T₁ • x  dom m₂  m₂(x)  dom m₁]

Например:

[3 ↦ true, 5 ↦ false]  [Klaus ↦ 3, John ↦ 7]  [Klaus ↦ true]

[3 ↦ true]  [Klaus ↦ 5]  []

Упражнения

1. Пусть база данных университета описана следующим образом (для простоты комментарии приведены на русском языке):

scheme

MAP_UNIVERSITY_SYSTEM =

class

type

Student,

Course,

CourseInfos = Course m Student-set,

University = Student-set  CourseInfos

value

 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  University

end

Определите функции, сигнатура которых приведена в данном описании.

Указания: воспользуйтесь явным стилем описания функций и операциями над отображениями.

Глава 2. Задание практикума

В данной главе формулируется задание практикума по составлению спецификаций на языке RSL для описания программных систем средней сложности. Здесь также приводятся конкретные варианты заданий и методические рекомендации по их выполнению.

1. Постановка задачи

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

1. Варианты заданий

1. Система учета автомобили – владельцы – доверенности.

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

1. Генеалогическое дерево.

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

1. Железнодорожное расписание станции.

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

1. Управление семафорами и стрелками на участке железной дороги.

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

1. Система поддержки составления расписания занятий.

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

1. Планирование автобусного движения в районе.

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

1. Заказ/учет товаров в бакалейной лавке.

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

1. Управление библиотекой.

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

1. Управление памятью на диске.

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

1. Информационное табло по состоянию авиарейсов.

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

1. Управление версиями программного проекта.

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

1. Система поддержки составления расписания поездов на железной дороге.

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

1. Управление процессами.

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

1. Протокол для передачи пакетов.

Специфицируется два набора операций, при помощи которых одна сторона, получив запрос на передачу сообщения, передает пакеты в линию и получает подтверждения, а вторая сторона, принимая пакеты, передает подтверждения.

1. Утилита make.

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

1. Методические рекомендации

При разработке спецификаций необходимо выбрать подходящую абстракцию данных и предложить набор операций (функций), обеспечивающих моделирование заданной программной системы. В качестве абстракции данных в зависимости от специфики решаемой задачи можно использовать множества, списки и отображения. Набор операций должен содержать операции, позволяющие накапливать в системе необходимую информацию, т.е. осуществлять наполнение некоторой информационной базы системы, способ представления которой определяется выбранным способом абстракции. Для этого обычно достаточно включить в состав операций следующие операции: инициализацию соответствующей информационной базы пустым значением, добавление в базу нового элемента и удаление указанного элемента из базы. При описании данных операций необходимо предусмотреть возможные ограничения на их выполнение, связанные с обеспечением непротиворечивости (консистентности) хранящейся в базе информации. Так, например, при формировании информационной базы системы поддержки составления расписания добавление нового занятия в расписание заданной группы может производиться только в том случае, если в указанное время у этой группы и преподавателя нет других занятий и свободна указанная аудитория. Одним из важных средств описания консистентного состояния являются инварианты, которые в RSL представляются либо в форме аксиом, либо в форме ограничений подтипов.

Характеристики

Список файлов книги