Языки спецификаций, используемые для формального описания свойств
программ, более высокого уровня, чем ЯП. Их можно классифицировать
по таким категориям: универсальные языки с общематематической
основой (например, 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], и поэтому студентам с математическим
мышлением будет интересно познакомиться с особенностями техник
спецификации и формального доказательства программ.
Анализ языков формальной спецификации программ
81
0
4 минуты
Темы:
Понравилась работу? Лайкни ее и оставь свой комментарий!
Для автора это очень важно, это стимулирует его на новое творчество!