рефераты конспекты курсовые дипломные лекции шпоры

Реферат Курсовая Конспект

Языки формальной спецификации.

Языки формальной спецификации. - раздел Программирование, Математические основы программирования. Теория схем программ. Семантическая теория программ Языки И Методы Формальной Спецификации, Как Средство Проектирования И Анализа...

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

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

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

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

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

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

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

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

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

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

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

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

Исполнимые спецификации, исполнимые модели. Этот подход предполагает разработку прототипов (моделей) систем для демонстрации возможности достижения поставленной цели и проведения экспериментов при частичной реализации функциональности. Примерами таких методологий и языков являются SDL, RSL (RAISE Specification Language).

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

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

Ограничения состоят из пред- и постусловий функций, процедур и других операций и инвариантов данных. Имеются расширения этого подхода для объектно-ориентированных спецификаций. В этом случае к спецификациям операций добавляются спецификации методов классов, а к инвариантам – инварианты объектов и классов. Языком, поддерживающим спецификацию ограничений, является RSL.

– Конец работы –

Эта тема принадлежит разделу:

Математические основы программирования. Теория схем программ. Семантическая теория программ

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

Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Языки формальной спецификации.

Что будем делать с полученным материалом:

Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:

Все темы данного раздела:

Программа как формализованное описание процесса обработки данных
Целью программирования является описание процессов обработки данных (в дальнейшем - просто процессов). Данные - это представление фактов и идей в формализованном виде, пригодном для п

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

Стандартные схемы программ
1.2.1. Базис класса стандартных схем программ Стандартные схемы программ (ССП) характеризуются базисом и структурой схемы. Базис класса фиксирует символы, из которых строятся схем

Свойства и виды стандартных схем программ
1.3.1. Эквивалентность, тотальность, пустота, свобода ССП S в базисе В тотальна (пуста), если для любой интерпретации I базиса В программа (S, I) останавливается (зацикливает

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

Рекурсивные схемы
1.5.1. Рекурсивное программирование Среди упомянутых выше методов формализации понятия вычислимой функции метод Тьюринга — Поста основан на уточнении понятия процесса вычислений, для чего

Трансляция схем программ
1.6.1. О сравнении класс сов схем. Программы для ЭВМ, будь-то программы, записанные на операторном языке, или программы на рекурсивном языке, универсальны в том смысле, что любую вычислиму

Обогащенные и структурированные схемы
1.7.1 Классы обогащенных схем Выделяют следующие классы обогащенных схем: класс счетчиковых схем, класс магазинных схем, класс схем с массивами. Классы счетчиковых и магази

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

Преобразователь предикатов.
Э. Дейкстра рассматривает слабейшие предусловия, т.е. предусловия, необходимые и достаточные для гарантии желаемого результата. «Условие, характеризующее множество всех начальных состояний

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

Правила верификации К. Хоара.
Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желае

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

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

Программирование параллельных вычислений
3.5.1. Основные понятия Исполнение процессов типичной параллельной программы прерывается значительно чаще, чем процессов, работающих в последовательной среде, так как процессы параллельной

Модели параллельных вычислений
Параллельное программирование представляет дополнительные источники сложности - необходимо явно управлять работой тысяч процессоров, координировать миллионы межпроцессорных взаимодействий. Для того

Основные определения
4.2.1. Теоретико-множественное определение сетей Петри Пусть мультимножество это множество, допускающее вхождение нескольких экземпляров одного и того же элемента. Сеть

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

Then begin
X1:=X1*Y; end; X2:=X2*Y; Y:=Y-1; end; write(X1); write(X2); endРисунок 4.5.

Анализ сетей Петри
Моделирование систем сетями Петри, прежде всего, обусловлено необходимостью проведения глубокого исследования их поведения. Для проведения такого исследования необходимы методы анализа свойств сами

Хотите получать на электронную почту самые свежие новости?
Education Insider Sample
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
Реклама
Соответствующий теме материал
  • Похожее
  • Популярное
  • Облако тегов
  • Здесь
  • Временно
  • Пусто
Теги