Язык спецификаций

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

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

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

Методы спецификацийПравить

ПризнакиПравить

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

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

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

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

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

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

CASL (Common Algebraic Specification Language)

Алгебра процессов^[1]:

EB³ (Entity-Based Black Box)

Логика^[1]:

Coq

См. такжеПравить

ПримечанияПравить

↑ ¹ ² ³ ⁴ ⁵ Habrias, Frappier, 2006.

ЛитератураПравить

Henri Habrias, Marc Frappier. Chapter 19 A Comparison of the Specification Methods // Software 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.

[_dd3a03fd7a414810-1] ¹ ² ³ ⁴ ⁵ Habrias, Frappier, 2006.

[1]