Руководство по Ada 2012

4.5.8 Квантифицированные выражения

Квантифицированные выражения позволяют записывать универсально и экзистенциально квантифицированные предикаты над контейнерами и массивами.

Синтаксис

quantified_expression ::= for quantifier loop_parameter_specification => predicate
| for quantifier iterator_specification => predicate

quantifier ::= all | some

predicate ::= boolean_expression

В тех местах Синтаксических Правил, где допускается выражение, может быть использовано quantified_expression вместо выражения, при условии, что оно окружено скобками.

Правила разрешения имён

Ожидаемый тип quantified_expression — любой булевый тип. predicate в quantified_expression также ожидается того же типа.

Динамические семантики

Для оценки quantified_expression сначала обрабатывается loop_parameter_specification или iterator_specification. Затем оценивается predicate для значений параметра цикла в порядке, указанном в loop_parameter_specification (см. 5.5) или iterator_specification (см. 5.5.2).

Значение quantified_expression определяется следующим образом:

Если quantifier равен all, выражение равно False, если вычисление любого predicate возвращает False; вычисление quantified_expression останавливается на этом моменте. В противном случае (каждый предикат был вычислен и возвратил True), выражение равно True. Любые исключения, возникающие при вычислении predicate, передаются.

Если quantifier равен some, выражение равно True, если вычисление любого predicate возвращает True; вычисление quantified_expression останавливается на этом моменте. В противном случае (каждый предикат был вычислен и возвратил False), выражение равно False. Любые исключения, возникающие при вычислении predicate, передаются.

Примеры

Пост условие для сортировочной процедуры по массиву A с типом индекса T можно записать:

Post => (A'Length < 2 или
(для всех I в A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))

Утверждение, что положительное число составное (в отличие от простого), можно записать:

pragma Assert (для некоторого X в 2 .. N / 2 => N mod X = 0);