Введение

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

Обзор

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