Узнать стоимость написания работы
Оставьте заявку, и в течение 5 минут на почту вам станут поступать предложения!
Ответы на вопросы

Конспект лекций по предмету "Надежность систем"


Анализ языков формальной спецификации программ

Языки спецификаций, используемые для формального описания свойств программ, более высокого уровня, чем ЯП. Их можно классифицировать по таким категориям: универсальные языки с общематематической основой (например, RAISE, Z, API, VDM и др.) [6.6-6.10]; языки спецификации проблемных областей (например, ЯП, языки спецификаций ПрО или доменов - DSL и др.) [6.11-6.14]; специализированные языки спецификации (например, языки таблиц, логики, равенств и подстановок и др.) [6.5]; языки, ориентированные на спецификацию параллельных процессов (например, CIP-L, Ada-68 Concurrent Pascal и др.) [6.11] (рис. 6.1).
Спецификация программы - это точное, однозначное и недвусмысленное описание программы с помощью математических понятий, терминов, правил синтаксиса и семантики языка спецификации. В языке спецификаций могут быть понятия и конструкции, которые нельзя выполнить на компьютере, они представляются последовательностью операций, функций, понятных для интерпретации.
Описание задачи в языке спецификации включает в себя описание общего контекста всех понятий, через которые определяются понятия, участвующие в формулировке задачи или в описании модели ПрО (домена).
Описание задачи дается в виде аксиом, утверждений, пред- и постусловий, требующих для их реализации не систем программирования, а специального аппарата для доказательства или верификации описания задач, в частности интерпретаторов или метасистем.

увеличить изображение Рис. 6.1.Категории языков спецификации
Универсальные языки спецификации (VDM, Z, RAISE и др.) имеют общематематическую основу и следующие виды средств:
· логики первого порядка, включая кванторы;
· арифметические операции;
· средства образования множеств с помощью логических формул и операций над множествами;
· средства описания конечных последовательностей (кортежей, списков) и операции над ними;
· средства описания конечных функций и операции над ними;
· средства описания древовидных структур;
· средства построения областей или множества объектов, включая произведения, объединения и рекурсивные определения;
· определение функций с помощью выражений и равенств, включая рекурсивные определения;
· процедурные средства ЯП (операторы присваивания, цикла, выбора, выхода);
· операции композиции, аргументами и результатами которых могут быть функции, выражения, операторы.
В VDM и RAISE нет средств описания графовых структур, управления и параллелизма, однако имеется механизм конструирования новых структур данных.
Языки спецификации областейвключают в себя следующие языки:
· спецификации доменов;
· описания взаимодействий;
· спецификации ЯП и трансляторов;
· спецификации БД и знаний;
· спецификации пакетов прикладных программ и др.
Каждый из этих языков имеет специализированные средства, отображающие специфические особенности соответствующей области.
Язык спецификации доменов DSL (Domain Specific Language) представляет некоторое подмножество языка программирования и специально средства для описания специальных проблем домена [6.14]. Он подразделяется на внешние и внутренние языки.Внешние языки (типа Unix, XML и др.) по уровню выше языка описания приложения. Описание в нем сводится к языку DSLспециальными генераторами или текстовыми редакторами, трансформирующими абстрактные понятия домена к понятиям языкаDSL. Внутренние языки (С, С++), а также языки Java, Smalltalk ограничены синтаксисом и семантикой основного базового языка программирования приложений.
Языки описания взаимодействий и параллельного выполнения в отличие от ЯП позволяют специфицировать процессы управления вычислениями, передачей сообщений и взаимодействием объектов в распределенных системах.
Метаязыки позволяют специфицировать контекстные зависимости синтаксиса ЯП, лексический и синтаксический анализтрансляторов с помощью регулярных выражений КС-грамматик в форме Бэкуса-Наура. Для спецификации семантики языков используется формализм равенств. Техника описания ЯП основывается на атрибутных грамматиках и абстрактных типах данных. Задача описания ЯП для перевода решаются путем использования денотационных, алгебраических и атрибутных подходов, а также логических терминов, ориентированных на верификацию [6.11-6.16].
Языки описания средств программированиявключают в себя языки, основанные на равенствах и подстановках с операционной семантикой (Лисп, Рефал); логические языки; языки операций (АPL) над последовательностями и матрицами; табличные языки; сети, графы [6.5, 6.11]. Язык логики предикатов с набором базисных функций используется для записи пред- и постусловий, инвариантов.
Отдельные операции логики предикатов используются также в языках логического программирования (например, Пролог).
Основой описания математических объектов являются равенства и подстановки. Для определения семантики равенства используется денотационное, операционное и аксиоматическое описание. Операционная семантика связана с подстановками (замена, продукция) и определяется в терминах операций, приводящих к вычислениям алгоритмов. При этом фиксируется порядок и динамика выполнения операций. Денотационный подход к семантике предпочитает статическое описание в терминах математических свойств объектов, а аксиоматической - специфицирует свойства объектов в рамках некоторой логической системы, содержащей правила вывода формул и/или интерпретаций.
Продукция или правила подстановки общего вида - это , где и - произвольные слова в фиксированном алфавите. Нормальный алгоритм Маркова [6.1] представляет собой упорядоченный набор правил, некоторые из них отмечены как завершающие. Применение правила к слову состоит в подстановке слова вместо самого левого слова в . Вычисление заканчивается, когда применяется завершающее правило, состоящее в порождении одного слова.
Языки спецификации программ или универсальные языки (Z, VDM, RAISE [6.5, 6.7-6.10]) базируются на аппарате математической логики и теории множеств и требуют от пользователей математической подготовки при применении их в трудно формализуемых областях -описание трансляторов с ЯП, системы реального времени, где правильность и точность программ основополагающие. На формальную спецификацию, разработку аксиом и теорем требуется несоизмеримо больше времени, чем в обычных языках программирования. Кроме того, формальные спецификации программ более громоздкие и требуют много времени при прокручивании таких программ за столом и интерпретации их на редких инструментальных средствах математического доказательства.
Эти особенности языков формальной спецификации препятствовали практическому их использованию. Их фактически отодвинул более конструктивный и наглядный стиль представления программ на языке UML, предоставив пользователям аппарат мышления объектами реального мира, диаграммным представлением их взаимодействия и многочисленными инструментами. В настоящее время интерес к формальным методам доказательства программ на основе спецификаций снова возник [6.15, 6.16], и поэтому студентам с математическим мышлением будет интересно познакомиться с особенностями техник спецификации и формального доказательства программ.


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

Поделись с друзьями, за репост + 100 мильонов к студенческой карме :

Пишем конспект самостоятельно:
! Как написать конспект Как правильно подойти к написанию чтобы быстро и информативно все зафиксировать.