И. Соммервилл - Инженерия программного обеспечения (1133538), страница 50
Текст из файла (страница 50)
При определении синтаксиса этих операций следует устаноэнть, какие для них необходимы параметры и каковы должны быть результаты операций. В общем случае входные параметры принадлежат или определяемому классу (э данном случае класс Е(эт) или более общему (родоэому) классу. Результаты операций также принадлежат тем жс классам или некоторому другому. например !п(айаг или Воо(еап; операция (.епййт нозаращает целое число.
Декларация импорта, объявляющая использование спецификации целых чисел, должна быть нключсна а спецификацию. Аксиомы, определяющие семантику абстрактного типа данных, написаны с использоэаннем ранее определенных операций. Операции над абстрактным типом данных обычно относятся к одному из двух кэассоэ. 1. Онврпции квястнрунрввпггнл, которые создают или изменяют объекты класса. Обычно их называют Сгаа(а (Создать), арба(е (Изменить), Абб (Добаэить) или, как э нашем случае, Сопя (Конструироэагггге).
2. ОнвРпмии лРвввРкгс которые возвращают атрибуты класса. Обычно им дают имена, соотэетстэующне имсналг атрибута, или имена, подобные Еча) (Зггачсние), Ое( (Получить) и т.п. 9. Формальные спецификации ПО 195 Хорошим эмпирическим правилом для написания алгебраической спецификации является создание аксиом для каждой операции конструирования с применением всех опе. раций проверки. Это означает, что если есть т операций конструирования и п операций проверки, то должно быль определено гп х и аксиом. Операции конструирования, связанные с абстрактным типом данных, часто очень сложны и могут определяться через другие операции конструирования и проверки. Если операции конструирования определены посредствои других операций, то необходимо определить операции проверки, используя более примитивные конструкции. В спецификации списка операциями конструирования являются Сгев(е, Сопя и Тв((, которые создают списки.
Операциями проверки являются Неао и (.еп9(В, которые используются для получения значений атрибутов списка. Операция Твй не является прими. тинной конструкцией, поэтому длл нее можно не определять аксиомы с использованием операций Неаб и (.еп9((з, но в такои случае Тай необходимо определить посредством примитивных конструкций. При написании алгебраических спецификаций часто используется рекурсия. Результат операции Тай — список, сформированный из входного списка путем удаления верхнего элемента.
Это определение подсказывает, как использовать рекурсию для построения данной операции. Операция определяется на пустых списках, затем рекурсивпо перехо. диг на непустые списки и завершается, когда результатом снова будет пустой список. Иногда проще понять рекурсивные преобразования, использул короткий пример. Предположим, что есть список [5, 7), где элемент 5 — начало (вершина) списка, а элемент 7 — конец списка. Операция Сопя([5, 7], 9) должна возвратить список [5, 7, 9], а операция Та)(, примененная к этому списку, должна возвратить список [7, 9]. Приведем последовательность рекурсивных преобразований, приводящую к этому результату.
Та! ([5, 7, 9]) = = Твй (Сопл ([5, 7), 9]) = = Сова (Та)! [[5, 7]), 9) = = Совз (Та)( (Сова ([5], 7)), 9) = = Сопз (Сопл (Та)! ([51], 7), 9) = = Сова (Савв (Тай (Сопв ([], 5)), 7), 9) = = Солз (Соав ([Сгва(е[, 7), 9) = = Сопз ([7], 9) = = [7, 9] Здесь систематически использовались аксиомы для Та)), что привело к ожидаемому результату. Аксиому для операции Неаб можно проверить подобным способом. Теперь рассмотрим, как эту методику можно использовать при разработке спецификации критической системы. Предположилк что имеется система управления вошгушным движением, целью которой является контроль за определенным сектором воздушного пространства.
В каждом контролируемом секторе может находиться несколько самолетов, имеющих различные идентификаторы. Из соображений безопасности эсе самолеты должны быть раз. ведены по высоте но крайней мере на 300 метров. В случае попьпки каким-либо самолетом нарушить это ограничение, система должна выдать предупреждающий сигнал. 196 Часть йк. Требования ВЕСТОН вит Зес1аг 1арюгЬ Р]ТЕОЕН, 8001ЕДМ Егаег добавнют самолет а сектор, если поаволпот условия безопасности (апе удавит самолет из свпора Мотю перемеаает самолет с одной амсотм на другую, если поэимвот услояил бваапасностн (оо(ар определяет амсву самолета Сгеа)в создает пуспй спнор Рцт добавляет саяолвт в спнор баз проамни условий бвмнвснастн Ь-красе гроввряет, есть ли самолет е сапере ОссцрЬб проверяет, доступна ли указанная амсата Елгег(Зас!ог, Сай-бйп, На(ОМ) -+ $ес(ог (лаю (Звсан, Сай-ббп)-о $ас1ог Мае(3ес!аг, Сярмйп, Нмйи) -+ Зюсцн (аа(ар(Зес1ог, Са]-Нйп)-+Ней)И! Сгеа!е-+ Зес(ог Р!я(Зюсюг, СН]чбрп, Не]йп!) ~ 8есюг (п-юрасе($есан,Сай-мйп) -гВоомап Оссцр]м) 8~от, М - Воомап Епиг ($, СЗ, Н) = Н(.зр (3, СЗ) бм 8 вгрбап(С о у во Юе) вЬН Оспгр)еб (8, Н) Нмп 8 ексербоп (Вмсота эвита) язв Рот($, СЗ, Й) (лне (Сгва1е, СЗ) = Сгеаю ексврбои (Самолет нв е секторе! (лвю (Рц! (3, СЗ), Н1) СЗ)= Н СЗ = С81 бмп 3 е1зв Рц) ((евв (3, СЗ), СЗ!, Н1) Моте (8, СЗ, Н] = Н 8 = Сгеам бип Смяв епербиг (В секторе нет самолетов) вЬН пот ]п-юрасе (8, СЗ) бип 8 аиербвт (Самолет не а секторе) еЬН Оссщяеб (3, Н) бмп 8 июврбон (Вмсота занята) е]зв Рц( ((емю (3, СЗ), СЗ, Н) — МО-НБВНТ - внстанта лоазмвавнвг, что значение амсотм не аозарзяюяю (виар (Сгабв, СЗ) = МО.НБОНТ аксврбап (Самолет не з секторе) (жбазг (]Чя (3, С81, Н!), СЗ! = Н СЗ =СЗ! Нми Й! ейа (оомгр (3, СЗ) Оссцр]вб (Стаю!е, Н] = 1зне Оссцрюб (Рцт (3, С$1, Н!), Н]= Н(Н1 >НягбН1-Н5300)аг(Н>Н! мн)Н-Н1 яЭОО]бмпаце е(ае Оссирмб (8, Н] ]п-красе (Сгеаю, СЗ] = ЬЬв 1п-зрзсв (Рот ($, С$1, Н1), СЗ) = Н С$ СЗ) бмп 1пю айв 1п.яраса (8, С$) г"-ис.
9.7, Сигнификация клоога Згстог, нргдсннголлннаего гокннф конпфпгирусмого оптдучнного гфоснгрпнснмо Чтобы упростить описание, я определил только ограниченное число операций над объсктомссктором. В реальной системе, консчно, будет намного больше операций и более сложными будут усл авил безопасности полста самолатов. Основные операции следующие. 9. Формальные спецификации ПО 197 1. Еп(ег (Ввод).
Добавляет самолет (представляемый идентификатором) в воздушное пространство на указанной высоте. На этой высоте или на расстоянии ближе 300 метров от него не должно быть другого самолета. 2. (нече (Выход). Удаляет укаэанный самолет из контролируемого сектора. Она применяется, если самолет перемещается в соседний сектор.
5. Моче (Перемещение). Перемещает самолет с одной высоты на другую. Опять про. веряются условия безопасности — расстояние между самолетами должно быть не менее 300 метров. 4. !.оо1а!р (Просмотр). Определяет текущую высоту самолета в секторе. Определение этих операций упростится, если определены также другие операции. 1. Сгеа1е (Создать). Стандартная операция для любого абстрактного типа данных. Она создает пустой экземпляр данного типа.
В нашем случае эта операция задает сектор, в котором отсугствуют самолеты. 2. Рц! (Поместить). Более простая версия операции Еп1ег. Она добавляет новый само. лет в сектор без проверки ограничений. 5. 1п-врасе (Проверка пространства). Возвращает значение истины, если указанный самолет находится в контролируемом секторе, в противном случае ее значение ложно. 4. Осоцр1еб (Занятый).
Возвращает значение истины, если внугри 50(ьметровой зоны по высоте есть самолет, в противном случае ее значение ложно. Простые операции определяются для того, чтобы впоследствии использовать их как блоки для компоновки более сложных опера!!ий. Алгебраическая спецификация класса 8ес1ог (Сектор) показана на рис. 9.7, По существу, основными операциями конструирования являются Сгеайз и Рц(, которые использованы в спецификациях других операций.
Оссцр!еб и !и-эрасе являются операциями проверки, которые определяют использование операций Сгеа!е и Рц!. Как выполняю гся эти и другие операции, легко понять из спецификации. 9.3. Спецификация поведения систем Простые алгебраические методы, описанные в предыдущем разделе, подходят для описания интерфейсов, когда операции, ассоциированные с объектом, не зависят от со.
стояния объекта. Тогда результаты любой операции не зависят от результатов предыдущих операций. Если зто условие не выполняется, алгебраические методы мо~ут стать гро. моздкими. Более того, я думаю, что алгебраические описания поведения систем часто искусственны и трудны для понимания. Альтернативным подходом к созданию формальных спецификаций, который широко используется в программных проектах, является спецификация, основанная на моделях системы. Такие спецификации используют модели состояний системы. Системные операции определяются посредством изменений состояний системной модели.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
