Формулы

Формулы, используемые в качестве предусловий и постусловий предикатов, есть формулы типизированного исчисления предикатов высших порядков. Подформула, входящая в предусловие или постусловие, может быть определена отдельно в виде описания формулы.

ОПИСАНИЕ-ФОРМУЛЫ::=

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 меняет позицию на противоположную. Все остальные позиции подформул считаются неизвестными.