Для спецификации семантики функций используются следующие подходы: табличный, алгебраический и логический, а также графический.
Функциональная спецификация представляет собой математически точное, но, как правило, не формальное описание поведения ПС. Формализованное представление функциональной спецификации имеет ряд достоинств, главным из которых является возможность применять некоторые виды автоматизированного контроля функциональной спецификации.
Под языком спецификаций понимается формальный язык, предназначенный для спецификации функций. В нем используется ряд средств, позволяющих фиксировать синтаксис и выражать семантику описываемых функций. Различие между языками программирования и языками спецификации может быть весьма условным: если язык спецификаций имеет реализацию на компьютере, позволяющую как-то выполнять представленные на нем спецификации (например, с помощью интерпретатора), то такой язык является и языком программирования, может быть, и не позволяющий создавать достаточно эффективные программы. Однако, для языка спецификаций важно не эффективность выполнения спецификации (программы) на компьютере, а ее выразительность. Язык спецификации, не являющийся языком программирования, может быть, тем не менее, полезен в процессе разработки ПС (для автоматизации контроля, тестирования и т.п.).
Один из вариантов записи спецификаций функций
Спецификация процедуры состоит из заголовка и описания функции, выполняемой процедурой. Заголовок содержит имя процедуры, номер, порядок и типы входных и выходных параметров. Входные могут, а выходные должны быть поименнованы.
Шаблон спецификации для процедурных абстракций:
pname = proc(…) returns (…)
requires //этот оператор задает ограничения, накладываемые на абстракцию
modifies //этот оператор идентифицирует все модиф.-е входные данные
effects //этот оператор описывает выполняемые функции.
end pname
Пример:
search = proc (int a[], int x) returns (int i)
requires массив а упорядочен по возрастанию.
effects Если элемент х принадлежит массиву а, то возвращается значение i такое, что a[i]=x; в противном случае значение i на единицу больше, чем значение верхней границы массива а.

Спецификация абстрактных типов состоит из заголовка, определяющего имя типа и имена его операций, и двух главных секций – секции описания и секции операций.
Шаблон спецификации абстрактных типов:
dname = data type is //список операций
Описание
//здесь приводится описание абстрактных данных
Операции
//здесь задаются спецификации для всех операций
end dname

Шаблон исключительных ситуаций:
В спецификацию процедуры добавляется предложение signals. Оно следует за предложением returns.
signals //здесь приводится список имен и результатов исключительных ситуаций.

Пример:
search = proc (int a[], int x) returns (int i)
signals(not_in, duplicate(int indl)) – 2 исключительные ситуации, одна без результата, а вторая в результате целое число indl, которое можно потом использовать в программе.