Главная страница « Информация « 5 курс « курс ФСиВП «

Варианты задания практикума по RSL. 2008-9 учебный год

Преподаватели 527, 528 групп:
канд. физ.-мат. наук Хорошилов Алексей Владимирович,
аспирант Корныхин Евгений Валерьевич,
аспирант Герлиц Евгений Анатольевич,
аспирант Монаков Александр Владимирович

Разработать на языке RSL спецификацию программного интерфейса определяемой вариантом задания системы в виде:

• явной моделе-ориентированной спецификации,
  

• неявной моделе-ориентированной спецификации,
  

• алгебраической спецификации.

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

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

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

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

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

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

6. Заказ и учет товаров в бакалейной лавке

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

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

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

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

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

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

13. Утилита make

14. Бронирование авиабилетов

15. Управление счетами в банке

16. Управление аптечной сетью

17. Туристическое бюро

18. Бюро кредитных историй

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• инициализацию информационной базы пустым значением (в RSL это выражается путем определения соответствующей константы),
  

• добавление в базу нового элемента,
  

• удаление указанного элемента из базы.

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

	type 
		Key, Data, Record = Key >< Data, 
		DataBase={| rs : Record-set :- is_wf_db(rs)|}
	value
		is_wf_db : Record-set -> Bool
		is_wf_db(rs) is (all k : Key, d1,d2 : Data :- 
		((k,d1) isin rs /\ (k,d2) isin rs) => d1 = d2)

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

	value
		add : Key >< Data >< DataBase -~-> DataBase
		add(k,d,db) as res
			post (k,d) isin db
		pre (k,d) ~ isin db

Предложенная спецификация является неполной, т.к. лишь частично описывает эффект от добавления нового элемента (k,d) в множество db. В частности, здесь игнорируется важный факт, что добавление элемента является единственным изменением, производимым функцией add над множеством db, и, следовательно, за исключением элемента (k,d) множества db и res должны полностью совпадать.

Требования ставят своей целью описать понятие автоматически транслируемой моделе-ориентированной спецификации в исполнимый код.

1. Проверить, что TypeChecker не выдает ошибок на спецификации

2. Проверить наличие функций по всем функциональным требованиям варианта

3. Для каждого типа проверить, что на всяком значении, подходящем под предусловие функции, функция определена правильно.

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

   • hd от пустого списка

   • tl от пустого списка

   • объединение отображений с потерей детерминированности ( [1 +> 2] union [1 +> 3] )

   • sort-типы

   • неявный let (кроме let x : T :- x isin s in ... end для недетерминированного выбора элемента из множества; более сложные формы неявного let (в том числе с более сложным условием) недопустимы)

   • константа chaos

   • конструкторы множеств и отображений, предполагающие обзор всех значений некоторого типа

   • кванторы, предполагающие обзор всех значений некоторого типа

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

5. Пост-условие неявной спецификации дополнительно к уже сказанному не должно содержать

   • побочный эффект

   • вызов функции без явной спецификации (потому что у такой функции нет "тела")

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

7. Заменить выражения с логическими константами на эквивалентные выражения без них.

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

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

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

Например, функция, возвращающая по списку пар и значению первого элемента значение второго элемента

   value
                 g: (A><B)-list >< A -~-> B
                 g(x, a) as b
                 post (a, b) isin elems x

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

Например, функция, по множеству пар и значению первого элемента возвращающая список значений второго элемента пар с данной первой, может иметь такое неявное определение:

    value
                 g: (A><B)-set >< A -~-> B-list
                 g(x, a) as bs
                 post   elems f(a, bs) <<= x ,

                 f: A >< B-list -> (A><B)-list
                 f(a, bs) is <. (a, b) | b in bs .>

Такие служебные функции могут носить характер обратной функции по отношению к определяемой неявным образом.

Первым делом следует четко разделить все функции на обсерверы, генераторы и трансформеры (они же - модификаторы). В алгебраической спецификации должны присутствовать все аксиомы вида "обсервер(генератор)" и "обсервер(трансформер)".

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

 value
		create: Unit -> Table,
		add: Key >< Value >< Table -> Table,
		count: Table -> Nat
	axiom
		[ count_create ]
		count( create() ) is 0,
		
		[ count_add ]
		forall t: Table, k: Key, v: Value :-
			count( add( k, v, t ) ) is count( t ) + 1

Судя по постановке задачи, count( add( 1, 1, add( 1, 2, create() ) ) is 1 ( т.к. add( 1, 1, add( 1, 2, create() ) is add( 1, 1, create() ) ). Однако по данной спецификации count( add( 1, 1, add( 1, 2, create() ) ) is 1 + count( add(1, 2, create() )) is 2 + count(create()) is 2, хотя должно быть 1. Ошибка заключается в том, что в аксиоме count_add не отражено свойство замены значения при имеющемся ключе. Аналогичная проблема существует и для тех целевых типов, в которых при добавлении значения для уже известного ключа происходит игнорирование добавленного значения.

Размещение на других ресурсах, а также коммерческое использование материалов, опубликованных в данном разделе, возможно только с разрешения авторов.