ГОСТ Р 59791—2021
Окончание таблицыА.1
Если Е является выражением в виде
Тогда 7(E)
=
Е12Логическое высказывание (iff Р Q)
7(E) = true, если I(P) = I(Q); в противном случае
7(E) = false
Высказывание или утверждение (cl: comment
7(E) = 1(Р)
“string” Р)
В), где N = {N1t ..., Nn} является набором обяза
тельных условий для высказывания
Е13Количественное высказывание (forall (N1 ... Nn)7(E) = true, если для каждой N-версии
J
в 7,
J(В) = true; в противном случае 7(E) = false
Е14Количественное высказывание (exists (N1 ... Nn)
В), где N = {N-i, ..., Nn} является набором обяза
тельных условий для высказывания
7(E) = true, если для части N-версий
J
в 7, J(В) яв
ляется истинным; в противном случае 7(E) = false
Правильно построенное выражение (cl: comment
“string”)
7(E) = true
Е17Импорт (cl: imports N)
7(E) = true
Е19Текстовая конструкция (cl: textT1 ... Tn)
7(E) = true, если I(T.,)= ... = I(Tn) = true; в против
ном случае 7(E) = false
Е20Заголовок (cl: ttl N T)
7(E) = true, если
ttlj(
N) = T; в противном случае
7(E) = false
Если E является выражением в виде
Тогда
1(E) =
Е21Утверждение в дискурсе (cl: indiscourse Т1 ... Тп)
1(E)
= true, если
I(Ti)
e
UD/
U
UD/*
для
1< i < n;
в
противном случае
1(E)
= false
Е22 Утверждение вне дискурса (cl: outdiscourse Т1 ...
Тп)
1(E)
= true, если
I(Ti)
<£
UD/
U
UD/*
для
1<i < n;
в
противном случае
1(E)
= false
Е23 Ограничение области
(cl: restricts N Т)
Текст
Т [Г]),
где
Г
— это текст Г, в котором каждое имя или
маркер последовательности
X
в списке boundlist
квантора заменяется на
(X N)
Таблица А.1 не включает в себя все синтаксические формы CLIF. Интерпретация остальных синтаксических
случаев зависит от их сопоставления с другими выражениями CLIF, интерпретация которых приведена в табли це
А.1. Перевод определяется в таблице А.2, где указан перевод Т [Е] для выражения Е.
Т аб л и ц а А.2 — Сопоставление дополнительных форм CLIF с основными
Если Е
То Е переводится в Т [ Е ]
=
Количественное высказывание (forall ((N1Т.,) ...) В )
Количественное высказывание
(forall (N.,) Т [ (forall (...) (if (Т1Nn) В) ]
Количественное высказывание (exists ((N1Т.,) ...) В )
Количественное высказывание
(exists (N.,) Т [ (exists (...) (and (Т1N.,) В) ]
Формы в левой части таблицы А.2 можно рассматривать как «синтаксический сахар» для своих переводов
справа, которые, соответственно, называются их синтаксической солью, а субдиалект CLIF без этих выражений
образует «соленый» CLIF.
А.4 Совместимость в CLIF
А.4.1 Синтаксическая совместимость
Соответствие синтаксиса CLIF абстрактному синтаксису CL обозначается с помощью обозначений в левом
столбце таблицы А.1, которые идентичны обозначениям в таблице 2. С их помощью можно определить полное
синтаксическое соответствие «соленого» CLIF в ходе проверки. Обратите внимание, что имена interpretedname и
31