rsl.formal.specifications.conspect (811084), страница 14
Текст из файла (страница 14)
Предлагаемым для вывода значением являетсязначение, возвращаемое выражением value_expr. Выражение output_exprвозвращает Unit значение в случае, если предложение произвести выводсовпадет с параллельным предложением произвести ввод по тому же каналу.6.23. Составные выражения (Structured Expressions)Синтаксис.structured_expr ::=local_expr ⏐let_expr ⏐if_expr ⏐case_expr ⏐while_expr ⏐until_expr ⏐for_expr6.23.1. Локальные выражения (Local Expressions)Синтаксис.local_expr ::=local opt-decl-string in value_expr endКонтекст и правила видимости. Контекстом объявления opt-decl-stringявляется само это объявление opt-decl-string и выражение value_expr.
Это71означает, что порядок определений в объявлении opt-decl-stringнесущественен.Контекстные условия. Входящие в локальное выражение объявления declдолжны быть совместимы.Максимальный тип выражения value_expr не должен включать в себяабстрактные типы, переменные и каналы, определенные в объявлениях decl.Атрибуты.
Максимальным типом локального выражения local_expr являетсямаксимальный тип содержащегося в нем выражения value_expr.Локальное выражение local_expr статически производит доступ к темнелокальным переменным и каналам (т.е. к переменным и каналам, неопределяемым в объявлении opt-decl-string), к которым статическиобращается входящее в его состав выражение value_expr.Семантика.
Результирующим воздействием локального выраженияlocal_expr является результирующее воздействие содержащегося в немвыражения value_expr, вычисленного в контексте определений, заданных вобъявлениях decl. Данное выражение value_expr вычисляется в каждоймодели, удовлетворяющей указанным определениям, и затем производитсянедетерминированный выбор между результирующими воздействиями этихвычислений.В конце вычисления выражения value_expr любое ожидающее обработкивзаимодействие по каналу, объявленному в объявлении opt-decl-string,замещается на stop.6.23.2. Let-выражения (Let Expressions)Синтаксис.let_expr ::=let let_def-list in value_expr endlet_def ::=typing ⏐explicit_let ⏐implicit_letexplicit_let ::=let_binding = value_exprimplicit_let ::=single_typing restrictionlet_binding ::=binding ⏐record_pattern ⏐list_patternКонтекстно-независимые расширения.
Выражение let_expr, содержащее всебе более одного определения let_def, является сокращенной формой записи72для некоторого числа вложенных let-выраженийопределением. То есть выражение let_expr вида:сединственнымlet let_def1, …, let_defn in value_expr endявляется сокращенной формой записи следующего выражения:let let_def1 in••••••let let_defn in value_expr endendКонтекст и правила видимости. В выражении let_expr вида:let let_def in value_expr endконтекстом определения let_def является выражение value_expr.Атрибуты.Максимальнымтипомвыраженияlet_exprявляетсямаксимальный тип содержащегося в нем выражения value_expr.В явном определении explicit_let максимальным контекстным типомконструкции let_binding является максимальный тип выражения value_expr.Выражение let_expr статически производит доступ к тем переменным иканалам, к которым статически обращаются входящие в его составопределения let_def и выражение value_expr.Указание типа typing не обращается статически ни к каким переменным иликаналам.Явное определение explicit_let статически производит доступ к темпеременным и каналам, к которым статически обращается входящее в егосостав выражение value_expr.Неявное определение implicit_let статически производит доступ к темпеременным и каналам, к которым статически обращается входящее в егосостав ограничение restriction.Семантика.
Выражение let_expr, содержащее одно определение let_def иимеющее вид:let let_def in value_expr endвычисляется следующим образом. Определение let_def представляетнекоторое множество моделей, как описано ниже. Указанное выражениеvalue_expr вычисляется в каждой такой модели и между результирующимиэффектами этих вычислений производится недетерминированный выбор.Различаются три вида определений let_def:• определение let_def в форме указания типа typing представляетмножество моделей, которые удовлетворяют определениям, заданныхуказанием типа typing;• определение let_def в неявной форме implicit_let представляет некотороеподмножество моделей, которые удовлетворяют определениям,73заданных указанием типа single_typing: тех из них, где выполняетсяограничение restriction;• определение let_def в явной форме explicit_let представляет множествомоделей, получаемое следующим образом.
Выражение value_exprвычисляется, и затем возвращаемое им значение сопоставляется сосвязыванием let_binding. Если данное значение соответствуетсвязыванию let_binding, результатом является некоторый наборопределений и искомое множество моделей содержит единственнуюмодель, удовлетворяющую этим определениям. Если же, напротив,данное значение не соответствует связыванию let_binding, то искомоемножество моделей пусто.6.23.3.
If- выражения (If Expressions)Синтаксис.if_expr ::=if logical-value_expr thenvalue_expropt-elsif_branch-stringopt-else_branchendelsif_branch ::=elsif logical-value_expr then value_exprelse_branch ::=else value_exprКонтекстно-независимые расширения. If-выражение if_expr, содержащееветви elsif_branch, представляет собой сокращенную форму записинекоторого числа вложенных if-выражений if_expr без ветвей elsif_branch.Выражение if_expr вида:if value_expr1 then value_expr1′elsif value_expr2 then value_expr2′•••elsif value_exprn then value_exprn′opt-else_branchendявляется сокращенной формой записи выражения:if value_expr1 then value_expr1′ elseif value_expr2 then value_expr2′ else••••••if value_exprn then value_exprn′ opt-else_branch endendend74Выражение if_expr вида:if value_expr1 then value_expr2 endявляется краткой записью выражения:if value_expr1 then value_expr2 else skip endКонтекстные условия.
В выражении if_expr вида:if value_expr1 then value_expr2 else value_expr3 endмаксимальным типом выражения value_expr1 должен быть тип Bool имаксимальные типы выражений value_expr2 и value_expr3 должны иметьнаименьшую верхнюю границу.Атрибуты. Для if-выражения вида:if value_expr1 then value_expr2 else value_expr3 endатрибуты определяются следующим образом. Максимальным типомуказанного выражения является наименьшая верхняя граница максимальныхтипов выражений value_expr2 и value_expr3.Рассматриваемое выражение if_expr статически обращается к темпеременным и каналам, к которым статически обращаются выраженияvalue_expr1, value_expr2 и value_expr3.Семантика.
Результирующее воздействие выражения if_expr состоит в том,чтобы определить применимую альтернативу и получить эффект от ееприменения. Выражение if_expr вида:if value_expr1 then value_expr2 else value_expr3 endвычисляется путем вычисления выражения value_expr1, которое возвращаетнекоторое булевское значение — тестовое значение. Если полученноетестовое значение равно true, вычисляется выражение value_expr2. Впротивном случае (значение тестового выражения равно false) вычисляетсявыражение value_expr3.6.23.4. Case-выражения (Case Expressions)Синтаксис.case_expr ::=case value_expr of case_branch-list endcase_branch ::=pattern → value_exprКонтекст и правила видимости.
В ветви case_branch контекстом образцаpattern является выражение value_expr.Контекстные условия. В выражении case_expr максимальные типывыражений value_expr, содержащихся в ветвях case_branch, должны иметьнаименьшую верхнюю границу.75Атрибуты. Максимальным типом case-выражения case_expr являетсянаименьшая верхняя граница максимальных типов выражений value_expr всоответствующих ветвях case_branch.В выражении case_expr максимальным контекстным типом образцов pattern вветвях case_branch является максимальный тип выражения value_expr.Выражение case_expr статически производит доступ к тем переменным иканалам, к которым статически обращаются содержащиеся в нем выражениеvalue_expr и ветви case_branch.Ветвь case_branch статически производит доступ к тем переменным иканалам, к которым статически обращается входящее в ее состав выражениеvalue_expr.Семантика.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
