rsl.formal.specifications.conspect (811084), страница 15
Текст из файла (страница 15)
Результирующее воздействие выражения case_expr состоит втом, чтобы вычислить выражение value_expr, определить соответствующуюветвь case_branch и затем вычислить выражение value_expr, содержащееся вэтой ветви. Выражение value_expr вычисляется и возвращает некотороезначение — тестовое значение. Затем просматриваются слева направо ветвиcase_branch до тех пор, пока данное тестовое значение не совпадет с какимлибо образцом pattern. Такое успешное сопоставление образца с тестовымзначением дает в результате некоторый набор определений.
В завершении вконтексте этих определений вычисляется соответствующее выражениеvalue_expr, содержащееся в ветви case_branch, на которой произошлоотождествление образца и тестового значения.Если ни на одной ветви case_branch не было достигнуто успеха всопоставлении тестового значения с соответствующими образцами,результирующимвоздействиемвыраженияcase_exprявляетсянедетерминированный выбор между результирующими воздействиями впустом множестве, т.е. swap.6.23.5.
While-выражения (While Expressions)Синтаксис.while_expr ::=while logical-value_expr do unit-value_expr endКонтекстные условия. Максимальным типом первого выражения value_exprдолжен быть тип Bool.Максимальным типом второго выражения value_expr должен быть тип Unit.Атрибуты. Максимальным типом выражения while_expr является Unit.Выражение while_expr статически обращается к тем переменным и каналам, ккоторым статически обращаются составляющие его выражения value_expr.Семантика. Результирующее воздействие выражения while_expr состоит втом, чтобы повторять вычисление второго выражения value_expr, покавычисление первого булевского выражения value_expr возвращает значение76true.Значением, возвращаемым выражением while_expr, является Unitзначение.Имеет место следующая эквивалентность:≡while value_expr1 do value_expr2 endif value_expr1 thenvalue_expr2 ; while value_expr1 do value_expr2 endelse skip end6.23.6. Until-выражения (Until Expressions)Синтаксис.until_expr ::=do unit-value_expr until logical-value_expr endКонтекстно-независимые расширения.
Выражение until_expr вида:do value_expr1 until value_expr2 endпредставляет собой краткую форму записи выражения:value_expr1 ; while ∼ value_expr2 do value_expr1 end6.23.7. For-выражения (For Expressions)Синтаксис.for_expr ::=for list_limitation do unit-value_expr endКонтекстные условия. Максимальным типом выражения value_expr долженбыть тип Unit.Контекстно-зависимые расширения. Выражение for_expr вида:for list_limitation do value_expr endпредставляет собой краткую форму записи выражения:let id = 〈 value_expr ⏐ list_limitation 〉 in skip end7.
Связывания (Bindings)Синтаксис.binding ::=id_or_op ⏐product_bindingproduct_binding ::=( binding-list2 )77Терминология. Значение может быть сопоставлено со связыванием bindingдля получения некоторого набора определений значений.Контекстные условия. Максимальный контекстный тип для связыванияbinding, представляющего собой операцию op, должен быть каким-либофункциональным типом, различимым с максимальным типом (типами)предопределенного значения (значений) операции op. Если операция opявляется инфиксной операцией infix_op, то типом параметра данногофункционального типа должен быть тип декартова произведения длины 2.Максимальным контекстным типом конструкции product_binding должен бытьтип декартова произведения той же длины, что и список binding-list2.В конструкции product_binding составляющие ее связывания binding должныбыть совместимы.Атрибуты. Контекст связывания binding определяет максимальныйконтекстный тип для данного связывания binding.
Для конструкций,содержащих в своем составе связывания binding, этот максимальныйконтекстный тип указывается в соответствующих разделах.В качестве максимального типа конструкции id_or_op, представляющейсобой связывание binding, принимается максимальный контекстный типданного связывания binding.В конструкции product_binding вида (binding1,…, bindingn) , контекстный типкоторой имеет вид t1 × … × tn, максимальными контекстными типамисвязываний binding1,…, bindingn являются типы t1, …, tn соответственно.Семантика. Совпадение некоторого значения v максимального контекстноготипа t со связыванием binding вида id_or_op дает следующее определение:id_or_op : t = vСовпадение значения некоторого декартова произведения (v1,…,vn)максимального контекстного типа t1 × … × tn со связыванием product_bindingвида (binding1,…, bindingn) дает набор определений, полученных присовпадении каждого значения vi максимального контекстного типа ti сосвязыванием bindingi.8.
Указания типа (Typings)Синтаксис.typing ::=single_typing ⏐multiple_typingsingle_typing ::=binding : type_exprmultiple_typing ::=binding-list2 : type_expr78commented_typing ::=opt-comment-string typingКонтекстно-независимые расширения. Все множественные указания типаmultiple_typing и typing-list являются сокращенной формой для единичныхуказаний типа. Так, множественное указание типа multiple_typing вида:binding1,…, bindingn : type_exprявляется сокращенной формой следующей записи:(binding1,…, bindingn) : type_expr × … × type_exprгде декартово произведение типов имеет длину n.Список typing-list вида:binding1 : type_expr1,…, bindingn : type_exprnявляется сокращенной формой следующей записи:(binding1,…, bindingn) : type_expr1 × … × type_exprnРазложение на единичные указания типа списка typing-list, включающегомножественные указания типа multiple_typing, начинается с разложения этихмножественных указаний типа multiple_typing.Атрибуты.
Максимальным типом единичного указания типа single_typingявляется максимальный тип выражения type_expr.В единичном указании типа single_typing максимальным контекстным типомсодержащегося в ней связывания binding является максимальный типсоответствующего выражения type_expr.Максимальное определение определения value_def, представляющего собойконструкциюcommented_typing,получаетсяпутемзамещениявсоставляющем ее указании типа typing типового выражения type_exprсоответствующим выражением максимального типа.Семантика.
Единичное указание типа single_typing вида:id_or_op : type_exprпредставляет определение некоторого значения — id_or_op вводится дляобозначения значения, тип которого представлен типовым выражениемtype_expr. Единичное указание типа single_typing вида:(binding1,…, bindingn) : type_expr1 × … × type_exprnпредставляет набор определений, представленных каждым единичнымуказанием типа:binding1 : type_expr1•••bindingn : type_exprn799.
Patterns (образцы)9.1. Общие замечанияСинтаксис.pattern ::=value_literal ⏐pure_value-name ⏐wildcard_pattern ⏐product_pattern ⏐record_pattern ⏐list_patternТерминология. Значение может сопоставляться с образцом pattern иливнутренним образцом inner_pattern (см. раздел 9.8), и такое сопоставлениеможет приводить к неудаче или успеху. В случае успеха результатомсопоставления является некоторый набор определений.Для каждого вида образцов pattern и внутренних образцов inner_patternзадается свой критерий успешного сопоставления, а также результирующийнабор определений для случая успешного сопоставления. Значение, котороесопоставляется с образцом pattern или внутренним образцом inner_pattern,называют ‘тестовым значением’.Атрибуты.
Контекст образца pattern или внутреннего образца inner_patternопределяет максимальный контекстный тип для данного образца pattern иливнутреннего образца inner_pattern. Для каждой конструкции, содержащей всвоем составе образцы pattern или внутренние образцы inner_pattern, этотмаксимальный контекстный тип указывается в соответствующих разделах.Контекстно-зависимые расширения. Для образца pattern или внутреннегообразца inner_pattern, представляющего собой литеральное значениеvalue_literal, имя name, образец запись record_pattern или образец равенствоequality_pattern, определено следующее контекстное условие: максимальныйтип, ассоциируемый с этим образцом pattern или внутренним образцомinner_pattern, должен быть меньше или равен его максимальногоконтекстного типа. Для этих образцов применяется неявное приведениетипов.
Неявное приведение типов представляет собой потенциальноеприведение (см. раздел 5.1) максимального типа к максимальномуконтекстному типу. Если неявное приведение типов не являетсятождественной функцией, то соответствующий образец pattern иливнутренний образец inner_pattern представляет собой сокращенную формуобразца записи, полученного путем применения указанного неявногоприведения типов:• Если неявное приведение типов является одной функцией f, то образецpattern или внутренний образец inner_pattern p представляет собойсокращенную форму образца записи record_pattern f(= p), если pявляется именем name, и f(p) в противном случае.80• Если неявное приведение типов является композицией функцийf1°…°fn (n ≥ 2), то образец pattern или внутренний образец inner_pattern pпредставляет собой сокращенную форму образца записи record_patternf1(…(fn(= p))…), если p является именем name, и f1(…(fn(p))…) впротивном случае.Аналогичные приведения типов имеют место в выражениях value_expr (см.раздел 6.1).9.2.
Литеральные значения (Value Literals)Контекстные условия. Для образца pattern или внутреннего образцаinner_pattern, представляющего собой литеральное значение value_literal (см.раздел 6.2), максимальный тип этого литерального значения value_literalдолжен быть меньше или равен максимального контекстного типауказанного образца pattern или внутреннего образца inner_pattern.Атрибуты.
Максимальным типом литерального значения value_literal,представляющего собой некоторый образец pattern, является максимальныйтип этого литерального значения value_literal.Семантика.• Успешное сопоставление: литеральное значение value_literal должнобыть равно тестовому значению.• Результирующие определения: нет.9.3. Имена (Names)Контекстные условия. Для образца pattern, представляющего собой имяname, это имя name должно представлять некоторое значение.Максимальный тип этого имени name (см. раздел 10) должен быть меньшеили равен максимального контекстного типа указанного образца pattern.Семантика.• Успешное сопоставление: значение, представленное именем name,должно быть равно тестовому значению.• Результирующие определения: нет.9.4.
Универсальные образцы (Wildcard Patterns)Синтаксис.wildcard_pattern ::=_Семантика.• Успешное сопоставление: все значения успешно сопоставляются суниверсальным образцом wildcard_pattern.81• Результирующие определения: нет.9.5. Образцы декартовы произведения (Product Patterns)Синтаксис.product_pattern ::=( inner_pattern-list2 )Контекстные условия. Максимальный контекстный тип образца декартовопроизведение product_pattern должен быть типом декартово произведение тойже длины, что и список внутренних образцов inner_pattern-list2.Составляющие данный образец внутренние образцы inner_pattern должныбыть совместимы.Атрибуты. В образце декартово произведение product_pattern вида(inner_pattern1,…, inner_patternn), максимальный контекстный тип которойимеет вид t1 × … × tn, максимальными контекстными типами внутреннихобразцов inner_pattern1,…, inner_patternn являются типы t1, …, tnсоответственно.Семантика.• Успешное сопоставление: пусть образец декартово произведениеproduct_pattern имеет вид:(inner_pattern1,…, inner_patternn)тогда тестовое значение должно быть декартовым произведением вида(v1,…,vn) и в дополнении к этому каждое значение vi должносопоставляться с соответствующим внутренним образцом inner_patterni.• Результирующие определения: набор определений, получаемый путемсопоставления каждого значения vi с внутренним образцомinner_patterni.9.6.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
