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

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

ВВЕДЕНИЕ

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

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

• описать эскизную модель (функциональности, поведения);

• доказать, что модель корректна (не противоречива, консистентна);

• детализировать (уточнить) модель;

• доказать, что детализация проведена корректно;

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

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

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

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

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

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

RSL поддерживает различные подходы к спецификации. Его универсальность была достигнута за счет интеграции языковых возможностей уже существующих языков. Полезно знать, из каких «первоисточников» складывался язык и сам RAISE метод.

Имеется несколько способов классификации подходов к спецификации. Например, различают моделе-ориентированные и свойство-ориентированные спецификации или спецификации, основанные на описании состояний (state-based) и описании действий (action-based). Единой классификации не существует, мы будем рассматривать следующие четыре класса подходов к спецификации:

• исполняемые (executable) спецификации,

• алгебраические или ко-алгебраические (co-algebraic),

• сценарные (use cases or scenarios) и

• ограничения (constraints).

Исполнимые спецификации, исполнимые модели (executable specifications, executable models). Этот подход предполагает разработку прототипов (моделей) систем для демонстрации возможности достижения поставленной цели и проведения экспериментов при частичной реализации функциональности. Примерами таких методологий и языков являются SDL [SDL], VDMTools [IFAD], явные определения функций (explicit function definitions) в RSL.

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

Сценарные (use case/scenario) спецификации описывают не непосредственно целевую систему, а способы ее использования или взаимодействия с ней. Оказывается, что такие косвенные описания, с одной стороны, позволяют судить о некоторых свойствах системы (тем самым, они, конечно, являются спецификациями), и, с другой стороны, такие спецификации могут служить хорошим руководством по использованию системы, что не всегда можно сказать о других видах спецификаций. Этот подход развивался многими авторами. Наибольшее распространение получили работы 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. В курсе лекций методам использования посвящено два блока. Первый – это методы проектирования с использованием формальных спецификаций; второй – это методы тестирования на основе формальных спецификаций. Таким образом, данное пособие предоставляет некоторый фундамент, но не исчерпывает всего материала курса.

1. Вводные замечания

1.1. Структура изложения материала

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

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

1. Необязательное вхождение х, где х – имя произвольной синтаксической категории, в металингвистическую формулу задается конструкцией opt- и определяется правилом:

opt-x ::=

nil-x │

x

при этом nil-x означает отсутствие х.

1. Возможные повторения в металингвистических формулах задаются с помощью конструкций -string, -list, -choice, ‑product и определяются правилами вида:

x-string ::=

x │

x x-string

x-list ::=

x │

x, x-list

x-list2 ::=

x, x │

x, x-list2

x-choice ::=

x │

x │ x-choice (в последней альтернативе ‘│’ является символом RSL)

x-choice2 ::=

x │ x │

x │ x-choice2 (в каждой из двух альтернатив ‘│’ является символом RSL)

x-product ::=

x│

x  x-product

x-product2 ::=

x  x │

x  x-product2

Если 'opt' появляется совместно с 'string' или 'list', 'opt' имеет наименьший приоритет. Это означает, что для любой синтаксической категории 'x' выполняются следующие правила:

opt-x-string ::=

nil-x-string │

x-string

opt-x-list ::=

nil-x-list │

x-list

Аналогично, если 'nil' появляется совместно с 'string' или 'list', 'nil' имеет наименьший приоритет.

1. Контекстные условия к произвольной синтаксической категории, входящей в альтернативу, задаются в виде напечатанного курсивом префикса к имени этой категории, например:

axiom_prefix_expr ::=

• logical-value_expr

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

restriction ::=

• readonly_logical-value_expr

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

Терминология. Эта секция содержит определения терминов и т.д. Определяемый термин в тексте выделяется курсивом.

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

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

Контекст (scope) и правила видимости. Секция содержит описание контекста и правил видимости.

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

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

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

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

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

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

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