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

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