Войти
A язык спецификаций - это формальный язык в информатике, используемый во время системного анализа, анализа требований и проектирование систем для описания системы на гораздо более высоком уровне, чем язык программирования, который используется для создания исполняемого кода для системы.
Языки спецификаций обычно не выполняются напрямую. Они предназначены для описания того, что, а не как. Действительно, если спецификация требований загромождена ненужными деталями реализации, считается ошибкой.
Общее фундаментальное предположение многих подходов к спецификации состоит в том, что программы моделируются как алгебраические или теоретико-модельные структуры, которые включают в себя набор наборов значений данных вместе с функциями над этими наборами. Этот уровень абстракции совпадает с представлением о том, что правильность поведения ввода / вывода программы имеет приоритет над всеми другими ее свойствами.
В подходе к спецификации, ориентированном на свойства (например, в CASL ), спецификации программ состоят в основном из логических аксиом, обычно в логической системе , в котором равенство играет важную роль, описывая свойства, которым функции должны удовлетворять - часто просто их взаимосвязь. Это отличается от так называемой ориентированной на модель спецификации в таких фреймворках, как VDM и Z, которые состоят из простой реализации требуемого поведения.
Спецификации должны подвергаться процессу доработки (заполнение деталей реализации), прежде чем они могут быть фактически реализованы. Результатом такого процесса уточнения является исполняемый алгоритм, который либо сформулирован на языке программирования, либо в исполняемом подмножестве имеющегося языка спецификации. Например, конвейеры Хартмана при правильном применении могут считаться спецификацией потока данных, которая является непосредственно исполняемой. Другой пример - модель Actor, которая не имеет конкретного содержимого приложения и должна быть специализированной, чтобы быть исполняемой.
Важное использование языков спецификации - это возможность создания доказательств правильности программы (см. средство доказательства теорем ).
