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

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

Value-expression в определениях констант и все предикаты в RSL – это детерминированные выражения.

Еще один важный случай, когда недетерминизм фактически запрещен – это предикаты, использующиеся как описания ограничений в аксиомах, пред- и пост-условиях, в других описаниях. Недетерминированный предикат тождественен false. Так, выражение:

axiom let b : Bool in b end

тождественно равно false, так как предикат, стоящий после слова axiom является недетерминированным. Следующий пример:

exists x : Char :- let y : Char in y end

Это выражение также равно false, так как ограничивающий предикат недетерминирован. Следовательно, выражение:

{ x | exists x : Char :- let y : Char in y end }

описывает пустое множество. Такие же правила использования предикатов справедливы в сокращенных описаниях списков и отображений, в описаниях подтипов и в имплицитной форме let-выражения.

Недетерминизм в case- и let-выражениях

Из перечисленных выше источников недетерминизма отдельного внимания заслуживает недетерминизм в case- и let-выражениях. Рассмотрим следующее определение множества, которое строится при помощи конструкторов empty и add:

type

Set == empty | add(Elem, Set)

axiom forall e, e₁, e₂ : Elem, s : Set :-

[no_duplicates]

add(e, add(e,s)) is add(e,s)

[unordered]

add(e₁, add(e₂,s)) is add(e₂, add(e₁,s))

Попробуем написать выражение, которое будет выбирать из значения типа Set некоторый (произвольный) элемент множества. В предположении, что

x – это переменная типа Set и

x empty

таким выражением может быть либо

let add(x, y) = s in x end

либо

case s of

add(x, y) -> x

end

Оба вышеприведенных выражения являются в общем случае недетерминированными, так как при данном определении Set , например, верно, что, если s= add(a, add(b, empty), то в силу аксиомы [unordered], верно, что s= add(b, add(a, empty ). Следовательно, и в случае let, и case значение этих выражений может равняться либо a, либо b, то есть выражения – недетерминированы.

Упражнения

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

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

1. Привести пример, когда комбинация двух недетерминированных функций дает детерминированный результат.

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

(a!1) || (b!1) || (x:=a?) || (x:=b?)

((a!1) || (b!1)) |=| ((x:=a?) || (x:=b?))

(a!1) || (b!1) || ((x:=a?) |=| (x:=b?))

1. Привести пример case- и let-выражений, которые дают недетерминированный результат. Перепишите спецификацию таким образом, чтобы все возможные поведения были представлены в форме детерминированных выражений, объединенных комбинатором |^|.

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

Постановка задачи. Варианты заданий. Требования и методические указания для выполнения задания.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Утилита make.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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