rsl.formal.specifications.conspect (811084)

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

Текст из файла

ВВЕДЕНИЕЯзыки и методы формальной спецификации, как средство проектирования ианализа программного обеспечения (ПО) появились более сорока лет назад.За это время было немало попыток разработать как универсальные, так испециализированные языки формальных спецификаций (ЯФС), которыемогли бы стать практическим инструментом разработчиков ПО, таким же,как, например, языки программирования. За свою недолгую историю ЯФСуже прошли через несколько периодов подъема и спада.

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

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

Еслирассматривать историю языков спецификации общего назначения(универсальных, не специализированных), то видно, что они развивались всоответствии со следующим представлением о «правильном порядке»разработке ПО:- описать эскизную модель (функциональности, поведения);- доказать, что модель корректна (не противоречива, консистентна);- детализировать (уточнить) модель;- доказать, что детализация проведена корректно;- повторять два предыдущих шага до тех пор, пока не будет полученаготовая программа.Установка на данную схему процесса разработки приводила какцентированному вниманию на средства обобщенного описанияфункциональности,средствауточнения,средствааналитическогодоказательства корректности в стиле традиционных математическихдоказательств.

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

Здесь эволюция заключалась во взаимномсближении графической и текстовой нотации на основе взаимныхкомпромиссов и ограничений. При этом участниками компромисса быланекоторая графическая нотация и языки программирования, опыт,накопленный в других языках формальных спецификаций, либоигнорировался, либо заимствовался с большим опозданием.ЯФС традиционно рассматривались как средство проектирования. Новыйвзгляд на ЯФС появился тогда, когда актуальной стала задача анализа ужесуществующего (legacy) ПО. Существенное продвижение на этом фронтебыло связано с направлением Объектно-Ориентированного Анализа (ООА).Идеи ООА во многом созвучны с Объектно-ОриентированнымПроектированием (ООП). Не удивительно, что оба эти направленияпредлагают близкие изобразительные средства для описания архитектуры иповедения систем. В последнее время наиболее известным средством такогорода является (преимущественно) графический язык UML.

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

Оказалось, чторазные виды приложений требуют совершенно различных подходов кспецификации и имеют непохожие друг на друга возможности для генерациитестов. В частности, одни виды спецификаций в большей степени пригодныдля генерации последовательностей тестовых воздействий (тестовыхцепочек), тогда как другие предоставляют удобные возможности длягенерации тестовых оракулов – программ, оценивающих результат,полученный в ответ на тестовое воздействие.Данное методическое пособие посвящено языку формальных спецификаций,разработанному в рамках методологии RAISE (Rigorous Approach to IndustrialSoftware Engineering) [RAISE-method]. Отсюда возникло и название языка –RSL (RAISE Specification Language) [RAISE-language].

Методология и языкбыли разработаны в рамках европейских программ ESPRIT 1 и ESPRIT 2.Задачей разработчиков методологии и языка было создание, с однойстороны, достаточно универсального средства и, с другой стороны,достаточно компактного и простого, ориентированного в первую очередь нена академических исследователей, а на инженеров. Сейчас, по прошествиипочти десяти лет после выхода описания языка, можно сказать, что авторамибыла проделана большая и полезная работа, они сумели скомпоноватьхорошо продуманный язык и вложить в него разнообразные возможности,используемые в других языках, тем не менее, задача-максимум – сделать егоинструментом инженеров – все еще не решена.

Однако из имеющихся4языков спецификации общего назначения RSL в наибольшей степениприблизился к языку для промышленного использования.RSL поддерживает различные подходы к спецификации. Егоуниверсальность была достигнута за счет интеграции языковыхвозможностей уже существующих языков. Полезно знать, из каких«первоисточников» складывался язык и сам RAISE метод.Имеется несколько способов классификации подходов к спецификации.Например, различают моделе-ориентированные и свойство-ориентированныеспецификации или спецификации, основанные на описании состояний (statebased) и описании действий (action-based).

Единой классификации несуществует, мы будем рассматривать следующие четыре класса подходов кспецификации:- исполняемые (executable) спецификации,- алгебраические или ко-алгебраические (co-algebraic),- сценарные (use cases or scenarios) и- ограничения (constraints).Исполнимые спецификации, исполнимые модели (executable specifications,executable models). Этот подход предполагает разработку прототипов(моделей) систем для демонстрации возможности достижения поставленнойцели и проведения экспериментов при частичной реализациифункциональности.

Примерами таких методологий и языков являются SDL[SDL], VDMTools [IFAD], явные определения функций (explicit functiondefinitions) в RSL.Алгебраические спецификации (algebraic specifications) предполагаютописание свойств композиций операций (композиции могут бытьпоследовательными, параллельными, с временными ограниченими и без).Преимуществом этого подхода является то, что в идеале можно полностьюабстрагироваться от структур данных, которые используются в качествевходных и выходных значений и, возможно, используются для сохранениявнутреннегосостояниямоделей.Основнойнедостаток–этонетрадиционность приемов спецификации, что затрудняет их внедрение впромышленных разработках.

В качестве примера зрелого (хотя и весьмаограниченного) языка алгебраических спецификаций можно назать ASN1,стандарт которого входит в группу стандартов, описывающих SDL [SDL].RSL предоставляет достаточно мощные средства для алгебраическихспецификаций (аксиомы).Сценарные (use case/scenario) спецификации описывают не непосредственноцелевую систему, а способы ее использования или взаимодействия с ней.Оказывается, что такие косвенные описания, с одной стороны, позволяют5судить о некоторых свойствах системы (тем самым, они, конечно, являютсяспецификациями), и, с другой стороны, такие спецификации могут служитьхорошим руководством по использованию системы, что не всегда можносказать о других видах спецификаций.

Этот подход развивался многимиавторами. Наибольшее распространение получили работы OMG группы[OMG] и продукты компании Rational Corporation [RUP]. СообществопользователейSDLиспользуеттакжехорошоизвестнуюистандартизованную нотацию MSC [MSC].Ограничения (constraints) состоят из пред- и пост-условий функций,процедур и других операций и инвариантов данных. Имеются расширенияэтого подхода для объектно-ориентироанных (ОО) спецификаций. В этомслучае к спецификациям операций добавляются спецификации методовклассов, а к инвариантам – инварианты объектов и классов. Классическимиязыками, поддерживающими спецификацию ограничений, является VDM[Jones] и Z[Z].

RSL предоставляет гибкие возможности для спецификацииограничений в форме имплицитных спецификаций функций и ограниченийподтипов. Идее спецификации ограничений следуют авторы, которыепредлагают средства для спецификации ОО ПО и средстваспецификационного расширения языков программирования: Eiffel [Eiffel],Larch [Larch], VDM [VDM-SL, VDM++], iContract [iContract], ADL [ADL].В данном методическом пособии собраны справочные материалы поосновным возможностям языка RSL. Их можно рассматривать как частьконспекта лекций, который читается на факультете ВМиК МГУ. Здесьописывается подмножество языка, которое не содержит один из видовмодулей – объекты. RSL не является языком ОО спецификации, и егообъекты совсем не похожи на объекты С++ или Java. Поэтому исключениеэтого вида модулей не вносит серьезных ограничений в возможностипользователей, при этом изложение основных концепций языка удаетсясделать более сжатым и понятным.Следует обратить внимание на то, что в пособие не вошли материалы,описывающие методы использования языка RSL.

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

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

Необязательное вхождение х, где х – имя произвольной синтаксическойкатегории, в металингвистическую формулу задается конструкцией opt- иопределяется правилом:opt-x ::=nil-x │xпри этом nil-x означает отсутствие х.2. Возможные повторения в металингвистических формулах задаются спомощью конструкций -string, -list, -choice, -product и определяютсяправилами вида:x-string ::=x│x x-stringx-list ::=x│x, x-listx-list2 ::=x, x │x, x-list2x-choice ::=x│x │ x-choice(в последней альтернативе ‘│’ является символом RSL)x-choice2 ::=x│x│x │ x-choice2 (в каждой из двух альтернатив ‘│’ является символом RSL)x-product ::=x│x × x-product7x-product2 ::=x×x│x × x-product2Если 'opt' появляется совместно с 'string' или 'list', 'opt' имеет наименьшийприоритет.

Это означает, что для любой синтаксической категории 'x'выполняются следующие правила:opt-x-string ::=nil-x-string │x-stringopt-x-list ::=nil-x-list │x-listАналогично, если 'nil' появляется совместно с 'string' или 'list', 'nil' имеетнаименьший приоритет.3. Контекстные условия к произвольной синтаксической категории,входящей в альтернативу, задаются в виде напечатанного курсивомпрефикса к имени этой категории, например:axiom_prefix_expr ::=• logical-value_exprздесь контекстное условие означает, чтосоответствующего выражения должен быть Bool.максимальныйтипrestriction ::=• readonly_logical-value_exprздесь контекстное условие означает, что соответствующее выражениедолжно быть доступно только для чтения и его максимальный тип долженбыть Bool.Терминология. Эта секция содержит определения терминов и т.д.Определяемый термин в тексте выделяется курсивом.Контекстно-независимые расширения.

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

Тип файла PDF

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

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов учебной работы