Языки и методы формальной спецификации (1158803), страница 10

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 10)

Ограничение restriction выполняется, если вычисление входящего в его состав выражения value_expr представляет собой сходящийся процесс, в результате которого возвращается значение true.

6.8. Выражения, задающие списки (List expressions)

Синтаксис.

list_expr ::=

ranged_list_expr ½

enumereted_list_expr ½

comprehended_list_expr

6.8.1. Списки, заданные диапазоном (Ranged List Expressions)

Синтаксис.

ranged_list_expr ::=

 integer-value_expr .. integer-value_expr 

Контекстные условия. Максимальным типом входящих в данную конструкцию выражений value_expr должен быть Int.

Атрибуты. Максимальным типом выражения ranged_list_expr является Int^.

Выражение ranged_list_expr статически производит доступ к тем переменным и каналам, к которым статически обращаются составляющие его выражения value_expr.

Семантика. Результирующее воздействие выражения ranged_list_expr заключается в возвращении списка целых чисел в диапазоне, ограниченном нижней и верхней границами. При этом вычисляется первое выражение value_expr и возвращает нижнюю границу i₁, затем вычисляется второе выражение value_expr и возвращает верхнюю границу i₂. Результирующий список содержит в возрастающем порядке все целые числа i такие, что i₁  i  i₂. Если i₁  i₂, список пуст.

6.8.2. Списки, заданные перечислением (Enumerated List Expressions)

Синтаксис.

enumerated_list_expr ::=

 opt-value_expr-list 

Контекстные условия. Максимальные типы составляющих данную конструкцию выражений value_expr должны иметь наименьшую верхнюю границу.

Атрибуты. Максимальным типом выражения enumerated_list_expr, имеющего в своем составе одно или более выражений value_expr, является t^, где t – это наименьшая верхняя граница максимальных типов этих составляющих выражений value_expr.

Максимальным типом выражения enumerated_list_expr, не имеющего в своем составе выражений value_expr (пустой список), является t^, где t – это типовая переменная, представляющая произвольный максимальный тип.

Выражение enumerated_list_expr статически производит доступ к тем переменным и каналам, к которым статически обращаются составляющие его выражения value_expr.

Семантика. Результирующее воздействие выражения enumerated_list_expr заключается в возвращении списка явно специфицированных значений. При этом результирующее воздействие выражения enumerated_list_expr вида value_expr₁,…, value_expr_n достигается путем вычисления слева направо значений v_i каждого выражения value_expr_i, после чего возвращается значение в виде списка v₁,…,v_n. Если конструкция value_expr-list отсутствует, возвращается пустой список.

6.8.3. Сокращенные выражения для списков (Comprehended List Expressions)

Синтаксис.

comprehended_list_expr ::=

 value_expr ½ list_limitation 

list_limitation ::=

binding in readonly_list-value_expr opt-restriction

Контекст и правила видимости. В выражении comprehended_list_expr контекст ограничения list_limitation расширяется до выражения value_expr, входящего в состав данного выражения.

Непосредственным контекстом конструкции binding, входящей в состав ограничения list_limitation, является ограничение restriction, входящее в тот же состав.

Контекстные условия. Входящее в состав ограничения list_limitation выражение value_expr должно представлять собой read-only выражение и его максимальный тип должен быть типом список.

Атрибуты. Максимальным типом выражения comprehended_list_expr является t^w, где t – это максимальный тип входящего в его состав выражения value_expr.

В конструкции list_limitation максимальным контекстным типом связывания binding является t, где t^w – это максимальный тип входящего в состав данной конструкции выражения value_expr.

Выражение comprehended_list_expr статически производит доступ к тем переменным и каналам, к которым статически обращаются составляющие его выражение value_expr и ограничение set_limitation.

Конструкция list_limitation статически производит чтение из тех же переменных, что и входящее в ее состав выражение value_expr. Если в данной конструкции присутствует ограничение restriction, то она также статически производит доступ к тем переменным и каналам, к которым статически обращается указанное ограничение restriction. Никакого другого статического доступа данная конструкция не имеет.

Семантика. Результирующее воздействие сокращенного выражения comprehended_list_expr состоит в том, чтобы возвратить список, генерируемый на основе некоторого другого списка.

Для каждой модели из списка моделей, представленного ограничением list_limitation (см. ниже), вычисляется выражение value_expr, входящее в состав исходного сокращенного выражения, и возвращаемое значение включается в результирующий список на соответствующую позицию. Список моделей, представленный ограничением list_limitation, обрабатывается слева направо.

По ограничению list_limitation список моделей строится следующим образом. Входящее в состав данного ограничения выражение value_expr возвращает некоторый список. Затем этот список просматривается слева направо, и каждый его элемент сопоставляется со связыванием binding для получения набора определений. Если для модели (она в точности одна), удовлетворяющей полученным определениям, выполняется ограничение restriction, то данная модель включается в результирующий список моделей на соответствующую позицию.

6.9. Выражения, задающие отображения (Map expressions)

Синтаксис.

map_expr ::=

enumereted_map_expr ½

comprehended_map_expr

6.9.1. Отображения, заданные перечислением (Enumerated Map Expressions)

Синтаксис.

enumerated_map_expr ::=

[ opt-value_expr_pair-list ]

value_expr_pair ::=

readonly-value_expr ↦ readonly-value_expr

Контекстные условия. В выражении enumerated_map_expr максимальные типы доменов входящих в него пар value_expr_pair должны иметь наименьшую верхнюю границу и максимальные типы областей значения тех же пар value_expr_pair должны иметь наименьшую верхнюю границу.

Составляющие пары value_expr_pair выражения value_expr должны представлять собой read-only выражения.

Атрибуты. Максимальным типом выражения enumerated_map_expr, имеющего в своем составе одну или более пар value_expr_pair, является t₁ t₂, где t₁ – это наименьшая верхняя граница максимальных типов доменов и t₂ – наименьшая верхняя граница максимальных типов областей значения этих пар value_expr_pair.

Максимальным типом выражения enumerated_map_expr, не имеющего в своем составе выражений value_expr (пустое отображение), является t₁ t₂, где t₁ и t₂ – это типовые переменные, представляющие произвольные максимальные типы.

Максимальным типом домена и максимальным типом области значения пары value_expr_pair являются максимальные типы первого и второго составляющего эту пару выражения value_expr соответственно.

Выражение enumerated_map_expr статически производит доступ к тем переменным и каналам, к которым статически обращаются составляющие его пары value_expr_pair.

Пара value_expr_pair статически производит чтение из тех переменных, из которых статически производят чтение составляющие его выражения value_expr, и не имеет другого статического доступа.

Семантика. Результирующее воздействие выражения enumerated_map_expr заключается в возвращении отображения явно специфицированных пар. При этом результирующее воздействие выражения enumerated_map_expr вида [value_expr_pair₁,…, value_expr_pair_n] состоит в вычислении слева направо пар значений (v₁, v₂) для каждой пары value_expr_pair_i, после чего возвращается значение в виде отображения, содержащего все эти пары. Результирующее воздействие пары value_expr_pair заключается в вычислении значения v₁ первого выражения value_expr, затем значения v₂ второго выражения value_expr, после чего возвращается пара (v₁, v₂). Если конструкция value_expr_pair-list отсутствует, возвращается пустое отображение.

6.9.2. Сокращенные выражения для отображений (Comprehended Map Expressions)

Синтаксис.

comprehended_map_expr ::=

[ value_expr_pair ½ set_limitation ]

Контекст и правила видимости. В выражении comprehended_map_expr контекст ограничения set_limitation расширяется до входящей в состав данного выражения пары value_expr_pair.

Атрибуты. Максимальным типом выражения comprehended_map_expr является t₁ t₂, где t₁ – это максимальный тип домена и t₂ –максимальный тип области значения входящей в данное выражение пары value_expr_pair.

Выражение comprehended_map_expr статически производит доступ к тем переменным и каналам, к которым статически обращаются входящие в его состав пара value_expr_pair и ограничение set_limitation.

Семантика. Результирующее воздействие выражения comprehended_map_expr заключается в возвращении отображения, пары которого получаются путем вычисления входящей в это выражение конструкции value_expr_pair во всех моделях, удовлетворяющих заданному ограничению. Для каждой модели из множества моделей, представленного ограничением set_limitation, вычисляется пара value_expr_pair. Если процесс вычисления указанной пары value_expr_pair сходится, результирующее значение пары включается в искомое отображение. Если вычисление такой пары не является сходящимся процессом, оно не вносит никакой пары в искомое отображение. Вычисление выражения comprehended_map_expr представляет собой сходящийся процесс.

6.10. Аппликативные выражения (Application Expressions)

Синтаксис.

application_expr ::=

list_or_map_or_function-value_expr actual_function_parameter-string

actual_function_parameter ::=

( opt-value_expr-list )

Контекстно-независимые расширения. Любое аппликативное выражение application_expr может быть разложено в выражение вида value_expr₁( value_expr₂ ).

Аппликативное выражение application_expr вида:

value_expr actual_function_parameter₁ … actual_function_parameter_n

где n > 1, является сокращенной записью выражения:

(…( value_expr actual_function_parameter₁ )…) actual_function_parameter_n

Аппликативное выражение application_expr вида value_expr() представляет собой сокращенную запись выражения value_expr(()).

Аппликативное выражение application_expr вида:

value_expr (value_expr₁,…, value_expr_n)

где n > 1, является сокращенной записью выражения:

value_expr ((value_expr₁,…, value_expr_n))

Характеристики

Список файлов книги