rsl.formal.specifications.conspect (811084), страница 11
Текст из файла (страница 11)
Если в даннойконструкции присутствует ограничение 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_expr6.9.1. Отображения, заданные перечислением (Enumerated MapExpressions)Синтаксис.enumerated_map_expr ::=[ opt-value_expr_pair-list ]56value_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, являетсяt1 ⎯⎯m→ t2, где t1 – это наименьшая верхняя граница максимальных типовдоменов и t2 – наименьшая верхняя граница максимальных типов областейзначения этих пар value_expr_pair.Максимальным типом выражения enumerated_map_expr, не имеющего всвоем составе выражений value_expr (пустое отображение), являетсяt1 ⎯⎯m→ t2, где t1 и t2 – это типовые переменные, представляющиепроизвольные максимальные типы.Максимальным типом домена и максимальным типом области значенияпары value_expr_pair являются максимальные типы первого и второгосоставляющего эту пару выражения value_expr соответственно.Выражение enumerated_map_expr статически производит доступ к темпеременным и каналам, к которым статически обращаются составляющиеего пары value_expr_pair.Пара value_expr_pair статически производит чтение из тех переменных, изкоторых статически производят чтение составляющие его выраженияvalue_expr, и не имеет другого статического доступа.Семантика.
Результирующее воздействие выражения enumerated_map_exprзаключается в возвращении отображения явно специфицированных пар. Приэтом результирующее воздействие выражения enumerated_map_expr вида[value_expr_pair1,…, value_expr_pairn] состоит в вычислении слева направо парзначений (v1, v2) для каждой пары value_expr_pairi, после чего возвращаетсязначение в виде отображения, содержащего все эти пары. Результирующеевоздействие пары value_expr_pair заключается в вычислении значения v1первого выражения value_expr, затем значения v2 второго выраженияvalue_expr, после чего возвращается пара (v1, v2). Если конструкцияvalue_expr_pair-list отсутствует, возвращается пустое отображение.6.9.2.
Сокращенные выражения для отображений (Comprehended MapExpressions)Синтаксис.comprehended_map_expr ::=[ value_expr_pair ⏐ set_limitation ]57Контекст и правила видимости. В выражении comprehended_map_exprконтекст ограничения set_limitation расширяется до входящей в составданного выражения пары value_expr_pair.Атрибуты. Максимальным типом выражения comprehended_map_exprявляется t1 ⎯⎯m→ t2, где t1 – это максимальный тип домена и t2 –максимальный тип области значения входящей в данное выражение пары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-stringactual_function_parameter ::=( opt-value_expr-list )Контекстно-независимые расширения.
Любое аппликативное выражениеapplication_exprможетбытьразложеноввыражениевидаvalue_expr1( value_expr2 ).Аппликативное выражение application_expr вида:value_expr actual_function_parameter1 … actual_function_parameternгде n > 1, является сокращенной записью выражения:(…( value_expr actual_function_parameter1 )…) actual_function_parameternАппликативное выражение application_expr вида value_expr()собой сокращенную запись выражения value_expr(()).58представляетАппликативное выражение application_expr вида:value_expr (value_expr1,…, value_exprn)где n > 1, является сокращенной записью выражения:value_expr ((value_expr1,…, value_exprn))Контекстные условия. В аппликативном выражении application_expr,имеющем только один фактический параметр actual_function_parameter,максимальный тип выражения value_expr должен быть либо списком, либоотображением, либо функциональным типом.
Кроме того, еслимаксимальный тип выражения value_expr является:• типом список — tω, то максимальным типом фактического параметраactual_function_parameter должен быть Int;• типом отображение — t1 ⎯⎯m→ t2, то максимальный тип фактическогопараметра actual_function_parameter должен быть меньше или равентипу t1;~ oads t , то максимальный тип• функциональным типом — t1 →2фактического параметра actual_function_parameter должен быть меньшеили равен типу t1.Атрибуты.
Максимальный тип аппликативного выражения application_expr,имеющего только один фактический параметр actual_function_parameter,определяется максимальным типом входящего в его состав выраженияvalue_expr. А именно, если максимальный тип данного выражения value_exprявляется:• типом список — tω, то максимальный тип аппликативного выраженияapplication_expr представляет собой тип t элементов этого списка;• типом отображение — t1 ⎯⎯m→ t2, то максимальный типаппликативного выражения application_expr представляет собой тип t2области значения этого отображения;~ oads t , то максимальный тип• функциональным типом — t1 →2аппликативного выражения application_expr представляет собой типрезультата t2.Максимальным типом фактического параметра actual_function_parameter,имеющего в своем составе одно выражение value_expr, являетсямаксимальный тип этого выражения value_expr.
Фактический параметрactual_function_parameter указанного вида статически производит доступ к темпеременным и каналам, к которым статически обращается выражениеvalue_expr.Аппликативное выражение application_expr, имеющее только одинфактический параметр actual_function_parameter, статически производитдоступ к тем переменным и каналам, к которым статически обращаютсявходящие в его состав выражение value_expr и фактический параметрactual_function_parameter.
Кроме того, если максимальным типом указанного~ oads t , товыражения value_expr является функциональный тип t1 →259аппликативное выражение application_expr статически производит доступтакже и к тем переменным и каналам, к которым статически обращается телофункции согласно описанию доступа oads.Семантика. Результирующее воздействие аппликативного выраженияapplication_exprзаключается в применении некоторого значения,представляющего собой список, отображение или функцию, к какому-либофактическому параметру.Результирующее воздействие аппликативного выражения application_exprвида value_expr1( value_expr2 ) состоит в вычислении выражения value_expr2для получения фактического параметра, затем вычислении значениявыражения value_expr1 и, наконец, применении полученного значения куказанному фактическому параметру.
При этом в зависимости от видазначения, которое применяется к фактическому параметру, такоеприменение выполняется следующим образом:• если данное значение представляет собой список, то фактическийпараметр должен принадлежать множеству индексов данного списка(множеству целых чисел в диапазоне от 1 до длины списка). В этомслучае возвращаемым значением становится элемент списка, стоящийв данной позиции. В противном случае результат применения являетсянедоспецифицированным.• если данное значение представляет собой отображение, тофактический параметр должен принадлежать домену отображения. Вэтом случае возвращаемым значением является то значение, в котороеотображается указанный фактический параметр, (если такое значение вточности одно) или недетерминированный выбор между значениями, вкоторые отображается данный фактический параметр, (если ихнесколько).
Если фактический параметр не принадлежит указанномуотображению,торезультатпримененияявляетсянедоспецифицированным.• если данное значение является функцией, то соответствующаяфункция применяется к указанному фактическому параметру.6.11. Квантифицированные выражения (Quantified Expressions)Синтаксис.quantified_expr ::=quantifier typing-list restrictionquantifier ::=∀⏐∃⏐∃!60Контекст и правила видимости. В квантифицированном выраженииquantified_expr контекстом входящих в него конструкций typing являетсяограничение restriction.Атрибуты. Максимальным типом квантифицированного выраженияquantified_expr является Bool.Квантифицированное выражение quantified_expr статически производитдоступ к тем переменным и каналам, к которым статически обращаетсявходящее в его состав ограничение restriction.Семантика.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
