stringtranslate.com

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

Язык спецификаций — это формальный язык в компьютерной науке, используемый во время системного анализа , анализа требований и проектирования систем для описания системы на гораздо более высоком уровне, чем язык программирования , который используется для создания исполняемого кода для системы. [1]

Обзор

Языки спецификаций обычно не выполняются напрямую. Они предназначены для описания того, что , а не того , как . Считается ошибкой, если спецификация требований перегружена ненужными подробностями реализации.

Распространенное фундаментальное предположение многих подходов к спецификации заключается в том, что программы моделируются как алгебраические или теоретико-модельные структуры, включающие наборы значений данных вместе с функциями над этими наборами. Этот уровень абстракции совпадает с представлением о том, что правильность поведения ввода/вывода программы имеет приоритет над всеми ее другими свойствами.

В подходе к спецификации, ориентированном на свойства (принятом, например, CASL ), спецификации программ состоят в основном из логических аксиом , обычно в логической системе , в которой равенство играет важную роль, описывая свойства, которым функции должны удовлетворять — часто просто через их взаимосвязь. Это контрастирует с так называемой спецификацией, ориентированной на модели, в таких фреймворках, как VDM и Z , которые состоят из простой реализации требуемого поведения.

Спецификации должны быть подвергнуты процессу уточнения (заполнения деталей реализации) до того, как они могут быть фактически реализованы. Результатом такого процесса уточнения является исполняемый алгоритм, который либо сформулирован на языке программирования, либо в исполняемом подмножестве языка спецификации. Например, конвейеры Хартмана , при правильном применении, могут считаться спецификацией потока данных , которая является непосредственно исполняемой. Другим примером является модель актора , которая не имеет определенного содержимого приложения и должна быть специализирована , чтобы быть исполняемой.

Важное применение языков спецификаций — создание доказательств корректности программ ( см. доказательство теорем ).

Языки

Смотрите также

Ссылки

  1. ^ Джозеф Гоген «Один, ни одного, сто тысяч языков спецификаций» Приглашенный доклад, Конгресс IFIP 1986 г., стр. 995-1004
  2. ^ Фукс, Норберт Э.; Швертель, Ута; Швиттер, Рольф (1998). "Попытка контролируемого английского языка — не просто еще один язык спецификации логики" (PDF) . Международный семинар по синтезу и преобразованию логического программирования . Конспект лекций по информатике. Том 1559. Springer. С. 1–20. doi :10.1007/3-540-48958-4_1. ISBN 978-3-540-65765-1.
  3. ^ "Самый простой язык формальных методов для разработчиков, создающих распределенные системы, микросервисы и облачные приложения" . Получено 28 мая 2024 г.
  4. ^ Линден, Теодор; Лоуренс Маркосян (1989). «Трансформационный синтез с использованием уточнения». В Richer, Mark (ред.). Инструменты и методы искусственного интеллекта . Ablex. стр. 261–286. ISBN 0-89391-494-0. Получено 6 июля 2014 г.

Внешние ссылки