ОПРЕДЕЛЕНИЕ-ПРЕДИКАТА ::= ИМЯ-ПРЕДИКАТА ОПИСАНИЕ-ПРЕДИКАТА
ИМЯ-ПРЕДИКАТА ::= ИДЕНТИФИКАТОР
Значением ОПИСАНИЯ-ПРЕДИКАТА является предикат, обозначаемый именем предиката.
ОПИСАНИЕ-ПРЕДИКАТА ::= ОПИСАНИЕ-ПРЕДИКАТА-ФУНКЦИИ |
ОПИСАНИЕ-ПРЕДИКАТА-ГИПЕРФУНКЦИИ
ОПИСАНИЕ-ПРЕДИКАТА-ФУНКЦИИ ::=
ЗАГОЛОВОК-ПРЕДИКАТА [pre ПРЕДУСЛОВИЕ]
ТЕЛО-ПРЕДИКАТА [post ПОСТУСЛОВИЕ]
ЗАГОЛОВОК-ПРЕДИКАТА ::=
( [ОПИСАНИЯ-АРГУМЕНТОВ]: ОПИСАНИЯ-РЕЗУЛЬТАТОВ )
ТЕЛО-ПРЕДИКАТА ::= БЛОК
ПРЕДУСЛОВИЕ ::= ФОРМУЛА
ПОСТУСЛОВИЕ ::= ФОРМУЛА
Значения аргументов предиката должны удовлетворять предусловию. По завершении исполнения тела предиката должно быть истинным постусловие, связывающее значения аргументов и результатов.
ОПИСАНИЯ-РЕЗУЛЬТАТОВ ::=
ИЗОБРАЖЕНИЕ-ТИПА [:blank:] ИМЯ-РЕЗУЛЬТАТА (, ИМЯ-РЕЗУЛЬТАТА)*
[, ОПИСАНИЯ-РЕЗУЛЬТАТОВ]
ИМЯ-РЕЗУЛЬТАТА ::= ИДЕНТИФИКАТОР | ИДЕНТИФИКАТОР ’
Имя вида имя’ используется для именования результирующего параметра при условии, что имя описано в качестве одного из аргументов с тем же типом. В императивной программе, получаемой трансформацией предикатной программы, результат с именем имя’ склеивается с соответствующим аргументом имя. Если тип аргумента имя параметризован (см. разд. 6.7), то значение параметра для типа результата имя’ может отличаться.
ОПИСАНИЯ-ГРУППЫ-АРГУМЕНТОВ ::=
ИЗОБРАЖЕНИЕ-ТИПА [:blank:] ИМЯ-АРГУМЕНТА (, ИМЯ-АРГУМЕНТА)* |
ИЗОБРАЖЕНИЕ-ТИПА-КАК-ПАРАМЕТРА
ОПИСАНИЯ-АРГУМЕНТОВ ::=
ОПИСАНИЯ-ГРУППЫ-АРГУМЕНТОВ [, ОПИСАНИЯ-АРГУМЕНТОВ]
ИМЯ-АРГУМЕНТА ::= ИДЕНТИФИКАТОР
assign (int from : int to) { to = from }
main (seq (string) argv : int ret_code) { ret_code = 0 }
power (real x, int p : real x’) { x’ = x^p; }
Пример 1. Определения предикатов
ОПИСАНИЕ-ПРЕДИКАТА-ГИПЕРФУНКЦИИ ::=
ЗАГОЛОВОК-ПРЕДИКАТА-ГИПЕРФУНКЦИИ [ПРЕДУСЛОВИЯ-ГИПЕРФУНКЦИИ]
ТЕЛО-ПРЕДИКАТА [ПОСТУСЛОВИЯ-ВЕТВЕЙ]
ЗАГОЛОВОК-ПРЕДИКАТА-ГИПЕРФУНКЦИИ ::=
( [ОПИСАНИЯ-АРГУМЕНТОВ] :
ОПИСАНИЯ-РЕЗУЛЬТАТОВ-ГИПЕРФУНКЦИИ )
ОПИСАНИЯ-РЕЗУЛЬТАТОВ-ГИПЕРФУНКЦИИ ::=
[ОПИСАНИЯ-РЕЗУЛЬТАТОВ-ВЕТВИ] [# МЕТКА-ВЕТВИ]
(: ОПИСАНИЯ-РЕЗУЛЬТАТОВ-ГИПЕРФУНКЦИИ)+
ОПИСАНИЯ-РЕЗУЛЬТАТОВ-ВЕТВИ ::= ОПИСАНИЯ-РЕЗУЛЬТАТОВ
МЕТКА-ВЕТВИ ::= МЕТКА
После двоеточия описываются параметры-результаты очередной ветви гиперфункции. Ветви гиперфункции именуются метками. Если в описании результатов ветви нет метки, то ветвь именуется целым - порядковым номером ветви начиная с 1. Исполнение гиперфункции завершается выбором одной из ветвей и вычислением значений результатов этой ветви. При этом результаты других ветвей не определены. Оператор перехода #имяВетви в теле предиката завершает исполнение гиперфункции ветвью с именем имяВетви.
ПРЕДУСЛОВИЯ-ГИПЕРФУНКЦИИ ::=
[ОБЩЕЕ-ПРЕДУСЛОВИЕ] (ПРЕДУСЛОВИЕ-ВЕТВИ)+
ОБЩЕЕ-ПРЕДУСЛОВИЕ ::= pre ПРЕДУСЛОВИЕ
ПРЕДУСЛОВИЕ-ВЕТВИ ::= pre МЕТКА-ВЕТВИ : ПРЕДУСЛОВИЕ
Отсутствие общего предусловия определяет допустимость произвольных значений аргументов в соответствии с их типами. Предусловие ветви определяет дополнительное условие на значения аргументов, при котором исполнение гиперфункции завершается выбором этой ветви. При этом значения аргументов должны удовлетворять общему предусловию. Предусловие последней ветви обычно не указывается, поскольку оно получается дополнением предусловий предыдущих ветвей.
ПОСТУСЛОВИЯ-ВЕТВЕЙ ::= (ПОСТУСЛОВИЕ-ВЕТВИ)+
ПОСТУСЛОВИЕ-ВЕТВИ ::= post МЕТКА-ВЕТВИ : ПОСТУСЛОВИЕ
Постусловие ветви связывает значения аргументов и результатов ветви. Ветвь без результатов постусловия не имеет.