Язык спецификаций — формальный язык , предназначенный для декларативного описания структуры, связей, свойств данных и способов их преобразований, (в отличие от активных языков) без явного упоминания порядка выполняемых действий и использования конкретных значений данных.

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

Различные языки спецификаций используются для описания структуры информационной системы, моделей предметной области и других задач, связанных с разработкой ПО и БД ( UML , ERD , DFD ) и могут иметь как текстовый, так и бинарный формат, а также графическое представление конструкций языка. Применяются они также для описания интерфейсов пользователя ( XUL , XAML ), шаблонов отчётов, преобразования документов, а также в качестве форматов передачи данных между приложениями в распределённых информационных системах ( XML , JSON , ). Ещё одно применение языков спецификации — описание структур баз данных, а именно — декларативная часть SQL обычно называется Data Definition Language ( DDL ). При синтаксическом анализе и разборе (парсинге) применяются языки спецификаций, например, форма Бэкуса — Наура и ( англ. augmented Backus-Naur form — расширенная форма Бэкуса — Наура) являются общепринятыми формальными языками спецификации сетевых протоколов и даже синтаксиса активных языков программирования; регулярные выражения аналогичны выше упомянутым нотациям, однако форма записи регулярных выражений в десятки раз компактнее, и хорошо разработаны алгоритмы парсинга с их помощью, а поддержка регулярных выражений осуществлена в подавляющем большинстве современных языков программирования.

Методы спецификаций

Признаки

Методы спецификации можно классифицировать по нескольким признакам :

• Парадигма ( смена состояний , алгебра, алгебра процессов , логика)
• Степень формальности (формальный, полуформальный, неформальный)
• Наличие графического представления
• Объектная ориентированность
• Поддержка параллелизма ( англ. concurrency )
• для имитационного моделирования системы ( англ. executability )
• Использование переменных
• Детерминированность/недетерминированность
• Логика (первого или более высокого порядка)
• Доказуемость
• Возможность проверки моделей
• Подавление событий (возможность может присутствовать, отсутствовать или не быть применимой к данному методу)

Языки спецификации по парадигмам

Использующие парадигму смены состояний :

• Action systems (системы действий)
• ДРАКОН
• Estelle
• LOTOS и e-LOTOS (Language of Temporal Ordering Specification)
• Сеть Петри и сеть Петри с объектами
• SAZ (комбинированный метод)
• Specification and Description Language (SDL)
• TLA⁺
• UML-B
• UML-Z
• VHDL
• Z-нотация

Алгебраическая парадигма :

• (Common Algebraic Specification Language)

Алгебра процессов :

• (Entity-Based Black Box)

Логика :

• Coq

См. также

• Компьютерный язык
• Язык программирования
• Модель акторов

Примечания

Литература

• Henri Habrias, Marc Frappier. Chapter 19 A Comparison of the Specification Methods // . — John Wiley & Sons, 2006. — 418 p. — ISBN 978-1-905-20934-7 .
• Bjørner, D. and Henson, M.C. Logics of Specification Languages. — Springer, 2007. — 646 p. — ISBN 9783540741077 .