Языки и методы формальной спецификации (1158803), страница 11
Текст из файла (страница 11)
Контекстные условия. В аппликативном выражении application_expr, имеющем только один фактический параметр actual_function_parameter, максимальный тип выражения value_expr должен быть либо списком, либо отображением, либо функциональным типом. Кроме того, если максимальный тип выражения value_expr является:
-
типом список — tw, то максимальным типом фактического параметра actual_function_parameter должен быть Int;
-
типом отображение — t1
t2, то максимальный тип фактического параметра actual_function_parameter должен быть меньше или равен типу t1;
-
функциональным типом — t1
oads t2, то максимальный тип фактического параметра actual_function_parameter должен быть меньше или равен типу t1.
Атрибуты. Максимальный тип аппликативного выражения application_expr, имеющего только один фактический параметр actual_function_parameter, определяется максимальным типом входящего в его состав выражения value_expr. А именно, если максимальный тип данного выражения value_expr является:
-
типом список — tw, то максимальный тип аппликативного выражения application_expr представляет собой тип t элементов этого списка;
-
типом отображение — t1
t2, то максимальный тип аппликативного выражения application_expr представляет собой тип t2 области значения этого отображения;
-
функциональным типом — t1
oads t2, то максимальный тип аппликативного выражения 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. Кроме того, если максимальным типом указанного выражения value_expr является функциональный тип t1 oads t2, то аппликативное выражение 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 restriction
quantifier ::=
½
½
Контекст и правила видимости. В квантифицированном выражении quantified_expr контекстом входящих в него конструкций typing является ограничение restriction.
Атрибуты. Максимальным типом квантифицированного выражения quantified_expr является Bool.
Квантифицированное выражение quantified_expr статически производит доступ к тем переменным и каналам, к которым статически обращается входящее в его состав ограничение restriction.
Семантика. Результирующее воздействие квантифицированного выражения quantified_expr заключается в возвращении булевского значения, зависящего от значения, которое возвращает некоторый предикат для каждой модели из некоторого множества моделей. Моделями, о которых идет речь, являются все модели, удовлетворяющие определениям, представленным указаниями типа typing-list.
Если в качестве квантора quantifier используется ", возвращаемое значение равно true тогда и только тогда, когда ограничение restriction выполняется для всех рассматриваемых моделей. Если квантором quantifier является $, возвращаемое значение равно true тогда и только тогда, когда ограничение restriction выполняется по крайней мере для одной рассматриваемой модели. И, наконец, если в качестве квантора quantifier используется $!, возвращаемое значение равно true тогда и только тогда, когда ограничение restriction выполняется в точности для одной рассматриваемой модели.
Вычисление квантифицированного выражения quantified_expr представляет собой сходящийся процесс.
6.12. Выражения эквивалентности (Equivalence Expressions)
Синтаксис.
equivalence_expr ::=
value_expr value_expr opt-pre_condition
pre_condition ::=
pre readonly_logical-value_expr
Контекстные условия. Максимальные типы входящих в данную конструкцию выражений value_expr должны иметь наименьшую верхнюю границу.
Выражение value_expr, входящее в состав предусловия pre_condition, должно представлять собой read-only выражение и его максимальный тип должен быть Bool.
Контекстно-зависимые расширения. Выражение эквивалентности equivalence_expr вида:
value_expr1 value_expr2 pre value_expr3
представляет собой сокращенную форму выражения:
( value_expr3 true ) value_expr1 value_expr2
Атрибуты. Максимальным типом выражения эквивалентности equivalence_expr является Bool.
Предусловие pre_condition статически производит чтение из тех переменных, из которых статически производит чтение составляющее его выражение value_expr, и не обращается статически ни к каким каналам.
Выражение эквивалентности equivalence_expr статически производит чтение тех переменных, к которым статически обращаются по чтению или записи входящие в него выражения value_expr. Оно также статически производит чтение переменных, из которых статически осуществляет чтение предусловие pre_condition (в случае его присутствия). Выражение эквивалентности equivalence_expr не обращается статически ни к каким каналам.
Семантика. Результирующее воздействие выражения эквивалентности equivalence_expr заключается в возвращении некоторого булевского значения, зависящего от того, обладают ли два входящих в него выражения value_expr одинаковым результирующим воздействием при вычислении каждого из них в текущем состоянии. Результирующие воздействия указанных двух выражений value_expr используются только для определения этого булевского значения и игнорируются в дальнейшем.
Значение, возвращаемое выражением эквивалентности equivalence_expr вида:
value_expr1 value_expr2
равно true тогда и только тогда, когда выражение value_expr1, вычисленное в текущем состоянии, представляет в точности такое же результирующее воздействие, что и выражение value_expr2 , вычисленное в том же состоянии. Это означает, что указанные два выражения value_expr должны представлять одно и то же результирующее воздействие в отношении возвращаемых значений, изменений состояния, предложений взаимодействия, внешних выборов, тупиковых ситуаций, внутренних выборов и расходимости.
Вычисление выражения эквивалентности equivalence_expr представляет собой сходящийся процесс.
6.13. Пост-выражения (Post-expressions)
Синтаксис.
post_expr ::=
value_expr post_condition opt-pre_condition
post_condition ::=
opt-result_naming post readonly_logical-value_expr
result_naming ::=
as binding
Контекст и правила видимости. В постусловии post_condition контекстом конструкции opt-result_naming является выражение value_expr.
Контекстные условия. В постусловии post_condition входящее в него выражение value_expr должно представлять собой read-only выражение и его максимальный тип должен быть Bool.
Контекстно-зависимые расширения. Пост-выражение post_expr вида:
value_expr1 post value_expr2
представляет собой сокращенную запись выражения:
value_expr1 as id post value_expr2
где id - это некоторый идентификатор уже вне контекста.
Пост-выражение post_expr вида:
value_expr1 post_condition pre value_expr2
представляет собой сокращенную запись выражения:
( value_expr2 true ) value_expr1 post_condition
Атрибуты. Максимальным типом пост-выражения post_expr является Bool.
Контекст постусловия post_condition определяет максимальный контекстный тип данного постусловия post_condition.
В пост-выражении post_expr максимальным контекстным типом постусловия post_condition является максимальный тип составляющего его выражения value_expr.
В конструкции result_naming максимальным контекстным типом связывания binding является максимальный контекстный тип ближайшего объемлющего постусловия.
Пост-выражение post_expr статически производит чтение тех переменных, к которым статически обращается по чтению или записи входящее в него выражение value_expr. Оно также статически производит чтение переменных, из которых статически осуществляет чтение предусловие pre_condition (в случае его присутствия). Пост-выражение post_expr не обращается статически ни к каким каналам.
Семантика. Результирующее воздействие пост-выражения post_expr заключается в возвращении некоторого булевского значения, которое зависит от результирующего воздействия выражения value_expr, вычисленного в пред-состоянии (pre-state). Результирующее воздействие выражения value_expr используется только для определения этого булевского значения и игнорируется в дальнейшем.
Значение, возвращаемое пост-выражением post_expr вида:
value_expr1 as binding post value_expr2