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

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

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

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

Так, например, приформировании информационной базы системы поддержки составлениярасписания добавление нового занятия в расписание заданной группы можетпроизводиться только в том случае, если в указанное время у этой группы ипреподавателя нет других занятий и свободна указанная аудитория. Одним изважных средств описания консистентного состояния являются инварианты,которые в RSL представляются либо в форме аксиом, либо в форме ограниченийподтипов.Кроме этих основных операций по наполнению информационной базысистемы полезно предусмотреть операции, позволяющие изменять отдельныеэлементы базы, а также осуществлять в базе поиск полезной с точки зренияразработчика спецификаций информации. Некоторые примеры таких операцийприводятся в описании заданий практикума, однако их набор может бытьрасширен по желанию разработчика спецификаций.30Глава 3.

Сценарий работы с редактором edenВ данной главе описывается сценарий работы с основным инструментомподдержки RAISE технологии – синтаксически управляемым редактором eden(entity editor), обеспечивающим ввод и редактирование текстов на языке RSL.Этот инструмент разработан датской компанией Computer Resources International– CRI.3.1.Начало работы с редакторомРедактор eden является синтаксически управляемым редактором, т.е. онгарантирует синтаксическую правильность любого вводимого с помощьюредактора текста спецификации на языке RSL и кроме того обеспечиваетстатическую проверку типов.

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

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

В ходесинтаксически управляемого редактирования в памяти системы формируетсяабстрактное синтаксическое дерево, представляющее собой вывод текста вграмматике базового языка. Процесс построения текста завершается, когда всевходящие в текст метапеременные будут заменены на соответствующиеконструкции базового языка, т.е. в тексте не останется ни одного вхожденияметапеременных (ни одного гнезда редактирования).Сценарий работы с редактором рассмотрим на примере построения текстамодуля QUEUE, содержащего следующую спецификацию очереди:QUEUE =classtypeElement,Queue = Element*valueempty : Queue = 〈〉,enq : Element × Queue → Queueenq(e,q) ≡ q ^ 〈e〉,31deq : Queue−∼→ Queue × Elementdec(q) ≡ (tl q,hd q)pre q ≠ emptyendДля начала работы с редактором создайте средствами UNIX директориюдля хранения своих файлов и объявите ее текущей.

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

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

Здесь содержится информация о текущейметапеременной, подлежащей редактированию (гнезде редактирования), исписок вариантов, определяющих замену текущей метапеременной навозможные конструкции языка RSL.3.2.Командное меню редактораВызов командного меню осуществляется по нажатию правой кнопки мыши.Вид окна редактора после выполнения этой операции приведен на рисунке 2.Рис. 2Каждый пункт командного меню содержит, как правило, несколько команд,поэтому каждому пункту меню соответствует выпадающее подменю, откуда ивыбираются команды редактора. При этом в подменю рядом с названиемкоманды указывается комбинация управляющих клавиш для ее вызова, такимобразом, вызов команды может производиться как с помощью меню, так ипосредством набора соответствующей комбинации управляющих клавиш.33••••••Кратко опишем назначение основных пунктов командного меню:transforms – позволяет при синтаксически управляемом редактированиизаменять текущее гнездо редактирования на некоторую конструкцию языкаRSL, список которых указывается в качестве подменю данного пункта.Обратите внимание на то, что содержимое подменю полностью совпадает сосписком альтернатив в поле подсказки, т.е.

выбор очередной альтернативыможет производиться как в подменю данного пункта, так и непосредственнов поле подсказки.edit – содержит команды, позволяющие вносить изменения в редактируемыйтекст.errors – позволяет изменять формат вывода сообщений об ошибках, т.е.выдавать эти сообщения в более развернутой или более краткой форме.save – содержит команды, позволяющие сохранять отредактированный текст,причем сохранение производится в текущей директории (при выборекоманд, начинающихся ключевым словом write) или текущей библиотеке(команды начинаются ключевым словом save).file – позволяет замещать текущее гнездо редактирования содержимымуказанного файла (при этом для успешной замены содержащийся в файлетекст должен быть синтаксически правильным) и, наоборот, запоминать вфайле с указанным именем выбранный фрагмент редактируемого текста вASCII формате.exit – команда выхода из редактора.3.3.Редактирование модуляНачальный этап редактирования модуля показан на рисунке 1.Редактируемый текст представляет собой единственное гнездо редактированияlib_module, это же гнездо является текущим (на экране выделено на фонеостального текста).

Выберите в поле подсказки или в пункте transformsкомандногоменюальтернативу lib_scheme, т.к.спецификацияразрабатываемого модуля представляет собой схему в терминологии RSL.Эффект выполнения команды иллюстрирует рисунок 3.Как видно из рисунка, теперь текст модуля содержит описание схемы,причем имя схемы совпадает с именем модуля. Текущим гнездомредактирования является class_expr, соответствующее следующей в порядкеобхода абстрактного синтаксического дерева метапеременной. Поле подсказкисодержит уже новый список альтернатив, определяющий возможные вариантыуточнения для метапеременной class_expr.Редактор eden позволяет наряду с синтаксически управляемымредактированием осуществлять редактирование в текстовом режиме.

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

Передвижение каретки на тот или иной символвнутри области ввода осуществляется с помощью мыши или нажатием клавиш^B (назад) и ^F (вперед), символы слева от каретки могут быть удаленынажатием клавиши Delete , символы справа от каретки удаляются нажатием^D. Если введенный текст является синтаксически правильным значением дляданного гнезда редактирования, выход из текстового режима осуществляется повыполнению любой команды, не относящейся к режиму текстовогоредактирования.В нашем случае для выхода из текстового режима достаточно (не нажимаяклавишу RETURN) переместить указатель мыши на любой фрагмент текста,лежащий вне области ввода, например, на имя схемы QUEUE и щелкнутьлевой кнопкой мыши.

После выхода из текстового режима для продолженияпроцесса редактирования щелкните левой кнопкой мыши на фрагменте class. Вид экрана после выполнения этих операций приведен на рисунке 4.35Рис. 4Отображенное на данном рисунке состояние редактора показывает, чторазбор введенного фрагмента текста произведен успешно (о чем свидетельствуетнулевое количество ошибок в строке статуса) и данному фрагментусоответствует синтаксическое дерево категории class_expr . Заметим, чтополностью аналогичный результат был бы получен в режиме синтаксическиуправляемого редактирования (см. рис. 3) при выборе альтернативыbasic_class_expr в списке альтернатив.Для продолжения процесса редактирования нажмите клавишу RETURN,по которой вызывается команда обхода соответствующего синтаксическогодерева слева направо с отображением на экране всех встречающихся в порядкеобхода гнезд редактирования.