Формулы, используемые в качестве предусловий и постусловий предикатов, есть формулы типизированного исчисления предикатов высших порядков. Подформула, входящая в предусловие или постусловие, может быть определена отдельно в виде описания формулы.
ОПИСАНИЕ-ФОРМУЛЫ ::=
formula ИМЯ-ФОРМУЛЫ ( ОПИСАНИЯ-АРГУМЕНТОВ [: ТИП-РЕЗУЛЬТАТА] ) =
ФОРМУЛА
ИМЯ-ФОРМУЛЫ ::= ИДЕНТИФИКАТОР
ТИП-РЕЗУЛЬТАТА ::= ИЗОБРАЖЕНИЕ-ТИПА
ОПИСАНИЕ-ФОРМУЛЫ вводит имя формулы для обозначения выражения, представленного ФОРМУЛОЙ. Переменные, входящие в ФОРМУЛУ, должны быть указаны в
ОПИСАНИЯХ-АРГУМЕНТОВ (см. разд. 6.3.1). Описание формулы помещается среди описаний модуля программы (см. разд. 4). ФОРМУЛА является выражением типа ТИП-РЕЗУЛЬТАТА. Если ТИП-РЕЗУЛЬТАТА не указан, то ФОРМУЛА имеет тип bool.
Использование формулы, определенной ОПИСАНИЕМ-ФОРМУЛЫ, в других формулах реализуется через вызов формулы.
ВЫЗОВ-ФОРМУЛЫ ::= ИМЯ-ФОРМУЛЫ (СПИСОК-ВЫРАЖЕНИЙ )
Описание формулы может быть рекурсивным: ФОРМУЛА в правой части описания может содержать рекурсивный вызов этой формулы. Не допускается взаимной рекурсии в описаниях двух разных формул. Другое требование: рекурсивный вызов должен находиться в позитивной позиции ФОРМУЛЫ. Понятия позитивной и негативной позиции определены ниже.
ФОРМУЛА ::= ВЫРАЖЕНИЕ | ( ФОРМУЛА ) | ВЫЗОВ-ФОРМУЛЫ |
! ФОРМУЛА | ФОРМУЛА & ФОРМУЛА | ФОРМУЛА or ФОРМУЛА |
ФОРМУЛА => ФОРМУЛА | ФОРМУЛА <=> ФОРМУЛА |
КВАНТОРНАЯ-ЧАСТЬ ФОРМУЛА
Все альтернативы приведенного правила, кроме первых трех, определяют формулы типа bool, т. е. предикаты. Операции «!», «&» и «or» имеют тот же смысл, что и для логических выражений. Операция => обозначает импликацию, <=> - логическое тождество.
КВАНТОРНАЯ-ЧАСТЬ ::=
КВАНТОР СПИСОК-ПОДКВАНТОРНЫХ-ПЕРЕМЕННЫХ . [КВАНТОРНАЯ-ЧАСТЬ]
КВАНТОР ::= КВАНТОР-ВСЕОБЩНОСТИ | КВАНТОР-СУЩЕСТВОВАНИЯ
КВАНТОР-ВСЕОБЩНОСТИ ::= ! | forall
КВАНТОР-СУЩЕСТВОВАНИЯ ::= ? | exists
Использование forall вместо «!» предпочтительно при вхождении квантора внутри формулы, поскольку «!» ассоциируется также с отрицанием.
СПИСОК-ПОДКВАНТОРНЫХ-ПЕРЕМЕННЫХ ::=
[ИЗОБРАЖЕНИЕ-ТИПА [:blank:]] ПОДКВАНТОРНАЯ-ПЕРЕМЕННАЯ
(, ПОДКВАНТОРНАЯ-ПЕРЕМЕННАЯ)*
ПОДКВАНТОРНАЯ-ПЕРЕМЕННАЯ ::= ИДЕНТИФИКАТОР
Приоритеты логических связок в порядке убывания следующие: !, &, =>, <=>, кванторы !, forall, ? и exists.
Определим понятие позиции, позитивной или негативной, для произвольного вхождения подформулы. Позиция ФОРМУЛЫ в качестве правой части ОПИСАНИЯ-ФОРМУЛЫ является позитивной. Допустим, формула X есть одна из следующих формул: A & B, A or B, !C, C => A, !y.A, ?y.A. Для перечисленных случаев подформулы A и B имеют ту же позицию, что формула X, а подформула C меняет позицию на противоположную. Все остальные позиции подформул считаются неизвестными.