Руководство по Ada (Ada 2022)
4.5.8 Квантифицированные выражения
Квантифицированные выражения предоставляют способ записи универсальных и экзистенциальных предикатных квантификаторов над контейнерами и массивами.
Синтаксис
quantified_expression ::=
for quantifier loop_parameter_specification => predicate
| for quantifier iterator_specification => predicate
for quantifier loop_parameter_specification => predicate
| for quantifier iterator_specification => predicate
quantifier ::= all | some
В тех местах, где Правила Синтаксиса допускают expression, может быть использовано quantified_expression вместо expression, при условии, что оно немедленно окружено круглыми скобками.
Правила разрешения имен
Ожидаемый тип quantified_expression — любой булевый тип. predicate в quantified_expression ожидается того же типа.
Динамическая семантика
Для оценки quantified_expression сначала выполняется разработка loop_parameter_specification или iterator_specification. Затем оценка quantified_expression выполняет итерацию и оценивает predicate для каждого условно полученного значения итерацией (см. 5.5 и 5.5.2).
Значение quantified_expression определяется следующим образом:
- Если quantifier равен all, выражение ложно, если оценка любого predicate даёт ложное значение; оценка quantified_expression прекращается в этот момент. В противном случае (каждый предикат был оценён и дал истинное значение), выражение истинно. Любое исключение, возникшее при оценке predicate, распространяется.
- Если quantifier равен some, выражение истинно, если оценка любого predicate даёт истинное значение; оценка quantified_expression прекращается в этот момент. В противном случае (каждый предикат был оценён и дал ложное значение), выражение ложно. Любое исключение, возникшее при оценке predicate, распространяется.
Примеры
Пример квантифицированного выражения в качестве пост условия для сортировки массива A с индексом подтипа T:
Post => (A'Length < 2 or else
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))
Пример использования квантифицированного выражения в качестве утверждения, что положительное число N составное (в отличие от простого):
