Специфика́ция програ́ммы, точное и, по возможности, полное описание назначения программы (программной системы), её функций, требований на входные данные, её результатов, особенностей функционирования и нефункциональных свойств таких как надёжность, отказоустойчивость, требований к ресурсам, и описание состава, структуры программы и её интерфейсов. То есть спецификация программы охватывает различные аспекты программы и её свойств, при этом разные аспекты часто описываются с разной полнотой. В этом случае говорят о частичных спецификациях или об абстрактных спецификациях, в которых нет всех деталей готовой программы (т. н. «реализации программы», англ. implementation). Высокоуровневая спецификация программы является одной из составных частей технического задания на разработку (см. ГОСТ 19.201-78 «Техническое задание. Требования к содержанию и оформлению»).
В силу того, что спецификация программы или части спецификации программы абстрагируются от несущественных деталей реализации, их часто рассматривают как модели программной системы или модели некоторых требований к программной системе или её свойств. Такой подход используется, например, в UML (см. CASE-технологии). Сами модели программ иногда называются спецификациями, например в Z, B-Method и Event-B.
Основными аспектами спецификации программы являются:
назначение (для решения каких задач можно или следует использовать);
состав (набор подпрограмм, функций, глобальных или локальных переменных, формальных параметров и др.);
структура (набор элементов и связей между ними), например, граф связей модулей по вызовам функций/подпрограмм;
поведение программной системы видимое извне (например, как результат функции, подпрограммы, через каналы ввода-вывода) или поведение, включая изменение внутреннего состояния программной системы (например, последовательность прохождения вершин на графе управления, значения локальных переменных);
способ использования (функциональные требования, которые должны быть выполнены перед началом использования и по завершении использования, ограничения по входным данным, ограничения по ресурсам и др.);
способ сборки (конфигурационные файлы, параметры конфигурирования, утилиты типа make) или способ её установки.
Помимо спецификации собственно программы рассматриваются спецификации характеристик внешнего по отношению к программе окружения, связанного с разработкой и эксплуатацией программных систем, например:
спецификация нефункциональных требований к программе (требований к ресурсам и аппаратной части, требований информационной безопасности, требований по переносимости, по отказоустойчивости и др.);
спецификация набора тестов или тестовой системы для данной программы.
Различные виды спецификаций отвечают различным целям их использования и различным ролям пользователя спецификации (программист-разработчик, тестировщик-верификатор, интегратор программного комплекса и др.), например:
для разработчика функциональная спецификация должна раскрывать интерфейсы разрабатываемой программы (каналы ввода-вывода данных), функцию программной системы (что должно быть получено в результате выполнения программы, какое поведение программы должно быть при получении тех или иных входных данных или других воздействий); кроме того, спецификация должна описывать ограничения, в которые разработчик должен уложиться (объём памяти, скорость вычислений или скорость реакции на входные воздействия);
для верификатора или разработчика тестов спецификация должна описывать условия корректного использования интерфейсов программы (например, ограничения на входные параметры, на аргументы функций, требования инициации глобальных данных перед обращением к интерфейсам) и критерии корректности результатов выполнения программы (например, требования к выходным данным, включая глобальные переменные, в зависимости от аргументов и состояния глобальных переменных перед вызовом программы).
Спецификации, которые описывают одну и ту же программу в одном и том же наборе аспектов, могут представлять собой иерархическую структуру, где верхние уровни описывают свойства программы в обобщённом (абстрактном) виде, а нижние в более детальном, уточнённом (англ. refined) виде. Переход от абстрактных спецификаций к уточнённым сам по себе называется уточнением (англ. refinement). Разбиение спецификации на слои уточнений позволяет разработчику сначала сконцентрироваться на общих требованиях к программе, а потом постепенно наращивать уровень подробностей в конструкции программы. Для верификатора разбиение спецификации на слои уточнений позволяет разбить задачу верификации большой системы на существенно более простые подзадачи верификации, сводящиеся к проверке правильности каждого перехода от более абстрактного слоя к его уточнению. Это же обстоятельство ослабляет требования к инструментам верификации и позволяет обходить ограничения таких инструментов.
Принято считать, что отличие спецификации программы от программы состоит в том, что она в большей степени ориентирована на понимание человеком, нежели на автоматическую обработку с помощью ЭВМ. Однако с ростом размеров программной системы и её сложности усложняется и понимание спецификации программы, по этой причине всё большую роль играют формальные или машиночитаемые формы спецификаций. «Потребителем» таких спецификаций, как правило, являются программные инструменты, например, инструменты верификации и генераторы тестов (тестирование на основе моделей и тестирование на основе спецификаций). В этом случае главным требованием к спецификации становится её пригодность не для понимания человеком, а для автоматической обработки имеющимися инструментами.
Если речь идёт о формальных спецификациях, то понятия и средства построения математических объектов, используемые в спецификациях, выходят далеко за рамки того, что характерно для типичных языков программирования. Это – равенства, системы подстановок и формулы исчисления предикатов, таблицы, графы (сети, диаграммы), операции над сложными объектами, средства описания взаимодействия процессов и процедурные средства высокого уровня, алгебраические системы. Набор парадигм программирования, в рамках которых строятся функциональные спецификации, мало отличается от парадигм в разработке программ, но при этом там, где возможно, используется декларативная, непроцедурная форма спецификации программы.
Известными языками формальной спецификации являются VDM (его развитие: VDM-SL и VDM++), Z (его развитие: B-Method, Event-B), Alloy, LOTOS (его развитие: E-LOTOS), TLA+, ACL2. Многие средства верификации спецификаций используют собственные нотации для представления спецификаций. Наряду с языками формальной спецификации постепенно в практику входят спецификационные расширения обычных языков программирования. Как правило, эти расширения позволяют описывать программные контракты (англ. software contract), предусловия на входные данные и постусловия на результаты. Например, такие средства спецификации уже вошли в современные версии стандартов языков программирования Ada (Ada-2012) и Spark-2014, Dafny, Whiley. Обсуждается введение средств спецификации в новых версиях стандарта C++.
Имеются спецификационные расширения языков программирования, например: JML для Java, ACSL (ANSI/ISO C Specification Language) для С, Spec# и Sing# для C#. Роль языков спецификации также выполняют языки моделирования. Часто они совмещают в себе возможности моделирования разных аспектов, например, архитектуры системы и функционального описания интерфейсов. Наиболее известным является язык моделирования UML и расширение его подмножества для спецификации архитектуры программно-аппаратных комплексов SysML и его альтернатива AADL. Для телекоммуникационных программно-аппаратных систем широкое распространение получили SDL и MSC, LOTOS и др.
Нередко спецификация программы создаётся на основе уже написанной реализации с встроенными в неё комментариями специального вида. Такие инструменты как Doxygen, Javadoc и их аналоги позволяют генерировать спецификации программ автоматически. При этом состав, структура программной системы, состав интерфейсов функций будут описаны полно и точно, а семантические характеристики (например, для формальных параметров и результатов функций) будут описаны лишь так, как они были описаны в соответствующих комментариях. Задачей генерации более точных спецификаций программ активно занимаются, например, в области статического анализа и верификации программ, но применимость таких спецификаций является ограниченной.