Спецификация процедуры состоит из заголовка и описания функции, выполняемой процедурой. Заголовок содержит имя процедуры, номер, порядок и типы входных и выходных параметров. Входные могут, а выходные должны быть поименнованы.
Шаблон спецификации для процедурных абстракций:
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, которое можно потом использовать в программе.