Язык спецификации
 | Эта статья нуждается в дополнительных ссылок для проверки . ( август 2016 г. ) |
Язык спецификации — это формальный язык в информатике, используемый во время системного анализа , анализа требований и проектирования систем для описания системы на гораздо более высоком уровне, чем язык программирования , который используется для создания исполняемого кода для системы. [1]
Обзор [ править ]
Языки спецификации обычно не выполняются напрямую. Они предназначены для описания того , что , а не как . Считается ошибкой, если спецификация требований перегружена ненужными деталями реализации.
Общее фундаментальное предположение многих подходов к спецификации заключается в том, что программы моделируются как алгебраические или теоретико-модельные структуры, которые включают в себя набор наборов значений данных вместе с функциями над этими наборами. Этот уровень абстракции совпадает с представлением о том, что правильность поведения ввода/вывода программы имеет приоритет над всеми ее другими свойствами.
В подходе к спецификации, ориентированном на свойства (принятом, например, в CASL ), спецификации программ состоят в основном из логических аксиом , обычно в логической системе , в которой равенство играет важную роль, описывая свойства, которым функции должны удовлетворять - часто просто по их взаимосвязи. Это контрастирует с так называемой модельно-ориентированной спецификацией в таких средах, как VDM и Z , которая состоит из простой реализации требуемого поведения.
Спецификации должны пройти процесс уточнения (заполнение деталей реализации), прежде чем они могут быть фактически реализованы. Результатом такого процесса уточнения является исполняемый алгоритм, который формулируется либо на языке программирования, либо в исполняемом подмножестве имеющегося языка спецификации. Например, конвейеры Хартмана при правильном применении можно рассматривать как спецификацию потока данных , которая является непосредственно выполняемой. Другим примером является модель актера , которая не имеет конкретного содержимого приложения и должна быть специализирована , чтобы быть исполняемой.
Важным применением языков спецификации является создание доказательств ( корректности программы см . средство доказательства теорем ).
Языки [ править ]
См. также [ править ]
- Формальная спецификация
- Независимая от языка спецификация
- Язык спецификации и описания
- Единый язык моделирования
Ссылки [ править ]
- ^ Джозеф Гоген Приглашенный доклад «Один, ни один, сто тысяч языков спецификаций», ИФИП , 1986 г., стр. 995-1004. Конгресс
- ^ Фукс, Норберт Э.; Швертель, Юта; Швиттер, Рольф (1998). «Попытка контролировать английский язык — не просто еще один язык логической спецификации» (PDF) . Международный семинар по синтезу и преобразованию логического программирования . Конспекты лекций по информатике. Том. 1559. Спрингер. стр. 1–20. дои : 10.1007/3-540-48958-4_1 . ISBN 978-3-540-65765-1 .
- ^ «Самый простой язык формальных методов для разработчиков, создающих распределенные системы, микросервисы и облачные приложения» . Проверено 28 мая 2024 г.
- ^ Линден, Теодор; Лоуренс Маркосян (1989). «Трансформационный синтез с использованием Refine» . В Ричере, Марк (ред.). Инструменты и методы искусственного интеллекта . Алекс. стр. 261–286. ISBN 0-89391-494-0 . Проверено 6 июля 2014 г.
Внешние ссылки [ править ]
СМИ, связанные с языками спецификаций, на Викискладе?
