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