rsl.formal.specifications.conspect (811084), страница 16
Текст из файла (страница 16)
Образцы записи (Record Patterns)Синтаксис.record_pattern ::=pure_value-name ( inner_pattern-list )Контекстные условия. В образце записи record_pattern имя name должнопредставлять некоторое значение и его максимальный тип должен бытьтипом чистой функции. Тип результирующей части этого функциональноготипа должен быть меньше или равен максимального контекстного типаданного образца записи record_pattern. Кроме того, если образец записьrecord_pattern имеет вид:name(inner_pattern1,…, inner_patternn)82(n>1)то параметрическая часть данного функционального типа должна иметь видt1 × … × tn.В образце записи record_pattern составляющие его внутренние образцыinner_pattern должны быть совместимы.Атрибуты.
В образце записи record_pattern вида name(inner_pattern)максимальным контекстным типом внутреннего образца inner_patternявляется параметрическая часть максимального типа указанного имени name.В образце записи record_pattern вида name(inner_pattern1,…, inner_patternn)максимальными контекстными типами внутренних образцов inner_pattern1,…,inner_patternn являются типы t1, …, tn соответственно, где типпараметрической части максимального типа имени name имеет вид t1 × … × tn.Семантика.• Успешное сопоставление: пусть образец запись record_pattern имеетвид:name(inner_pattern1,…, inner_patternn)(n>1)и пусть v — тестовое значение, тогда должны существовать значенияv1,…,vn такие, что:v = name(v1,…, vn)и в дополнении к этому каждое значение vi должно сопоставляться ссоответствующим внутренним образцом inner_patterni.• Результирующие определения: набор определений, получаемый путемсопоставления каждого значения vi с внутренним образцомinner_patterni, при этом значения v1,…,vn недетерминированновыбираются таким образом, чтобы были выполнены условияуспешного совпадения, описанные выше.9.7.
Образцы списки (List Patterns)Синтаксис.list_pattern ::=enumerated_list_pattern ⏐concatenated_list_patternКонтекстные условия. Максимальным контекстным типом образца спискаlist_pattern должен быть какой-либо списочный тип.9.7.1. Образцы списки, заданные перечислением (Enumerated ListPatterns)Синтаксис.enumerated_list_pattern ::=〈 opt-inner_pattern-list 〉83Контекстные условия. Составляющие данную конструкцию внутренниеобразцы inner_pattern должны быть совместимы.Атрибуты. Максимальным контекстным типом каждого внутреннегообразца inner_pattern является тип элемента максимального контекстноготипа содержащего их образца списка list_pattern.Семантика.• Успешное сопоставление: пусть образец список enumerated_list_patternимеет вид:〈inner_pattern1,…, inner_patternn〉(n>0)тогда тестовое значение должно представлять собой список вида〈v1,…,vn〉 и в дополнении к этому каждое значение vi должносопоставляться с соответствующим внутренним образцом inner_patterni.• Результирующие определения: набор определений, получаемый путемсопоставления каждого значения vi с внутренним образцомinner_patterni.9.7.2.
Образцы списки, заданные конкатенацией (Concatenated ListPatterns)Синтаксис.concatenated_list_pattern ::=enumerated_list_pattern ^ inner_patternКонтекстные условия. Входящие в данную конструкцию образец списокenumerated_list_pattern и внутренний образец inner_pattern должны бытьсовместимы.Атрибуты. Максимальным контекстным типом образца спискаenumerated_list_pattern и внутреннего образца inner_pattern являетсямаксимальный контекстный тип содержащего их образца спискаconcatenated_list_pattern.Семантика.• Успешное сопоставление: пусть образец список concatenated_list_patternимеет вид:enumerated_list_pattern ^ inner_patternтогда тестовое значение должно представлять собой список вида l1 ^ l2,где l1 сопоставляется с образцом списком enumerated_list_pattern и l2сопоставляться с внутренним образцом inner_pattern.• Результирующие определения: набор определений, получаемый путемсопоставления списка l1 с образцом списком enumerated_list_pattern исписка l2 с внутренним образцом inner_pattern.849.8.
Внутренние образцы (Inner Patterns)Синтаксис.inner_pattern ::=value_literal ⏐id_or_op ⏐wildcard_pattern ⏐product_pattern ⏐record_pattern ⏐list_pattern ⏐equality_patternДля внутренних образцов используется общая для всех образцовтерминология, атрибуты и контекстно-зависимые расширения (см. раздел9.1).Определения всех перечисленных здесь конкретных видов образцов кромеid_or_op и equality_pattern даны в разделах 9.2 – 9.7.9.8.1.
Идентификаторы или операции (Identifiers or Operators)Контекстные условия. Максимальный контекстный тип для внутреннегообразца inner_pattern, представляющего собой операцию op, должен бытькаким-либо функциональным типом, различимым с максимальным типом(типами) предопределенного значения (значений) операции op. Еслиоперация op является инфиксной операцией infix_op, то типом параметраданного функционального типа должен быть тип декартова произведениядлины 2.Атрибуты. В качестве максимального типа конструкции id_or_op,представляющей собой внутренний образец inner_pattern, принимаетсямаксимальный контекстный тип данного внутреннего образца inner_pattern.Семантика.• Успешное сопоставление: все значения максимального контекстноготипа успешно сопоставляются с идентификатором или операциейid_or_op.• Результирующие определения: пусть v является тестовым значением и t— максимальным контекстным типом конструкции id_or_op, тогдарезультирующим является следующее определение:id_or_op : t = v9.8.2.
Образцы равенства (Equality Patterns)Синтаксис.equality_pattern ::== pure_value-name85Контекстные условия. В образце равенстве equality_pattern имя name должнопредставлять некоторое значение.Максимальный тип этого имени name (см. раздел 10) должен быть меньшеили равен максимального контекстного типа содержащего его образцаравенства equality_pattern.Семантика.• Успешное сопоставление: значение, представленное именем name,должно быть равно тестовому значению.• Результирующие определения: нет.10.
Имена10.1. Общие замечанияСинтаксис.name ::=id ⏐( op )Атрибуты. Если имя name представляет некоторую схему, то для негоопределен максимальный класс, т.е. максимальный класс ассоциируемого сданным именем классового выражения. В случае параметризованной схемыу этого имени есть также некоторый формальный параметр схемы. Если имяname представляет какой-либо тип, значение, переменную или канал, то сним (с именем) ассоциируется некоторый максимальный тип. Ниже длякаждой из указанных альтернатив определены свои конкретные атрибуты.Семантика.
Имя name представляет некоторую сущность, которая являетсясхемой, типом, значением, переменной или каналом.10.2. Идентификаторы (Identifiers)Атрибуты. Если имя name представляет собой идентификатор id, то егоатрибутами являются атрибуты данного идентификатора id.Семантика.
Идентификатор id представляет сущность, с которой он связансоответствующим определением.10.3. Операции (Operators)Контекст и правила видимости. В конструкции name, являющейсяоперацией op, видны все предопределенные значения операций.Атрибуты. Максимальным типом имени name, представляющим собойоперацию, является максимальный тип этой операции op.Семантика. Операция op представляет сущность, с которой она связанасоответствующим определением.86Скобки превращают операцию op в функцию, которую можно применять впрефиксной нотации как аппликативное выражение (см. раздел 6.10). Сучетом того, что операция op может быть префиксной prefix_op илиинфиксной infix_op, это означает выполнение следующих эквивалентностей:prefix_op value_expr ≡ (prefix_op )( value_expr )value_expr1 infix_op value_expr2 ≡ (infix_op )( value_expr1, value_expr2 )11.
Идентификаторы и операции11.1. Общие замечанияСинтаксис.id_or_op ::=id ⏐opop ::=infix_op ⏐prefix_opТерминология. Любое встречающееся в тексте вхождение идентификатораили операции (id_or_op, id или op) может быть связано либо с ихопределением — точка определения (defining occurrence), либо с ихприменением или использованием — точка использования (appliedoccurrence).Точками определения считаются следующие вхождения:• идентификатора(идентификаторов)id,встречающегосянепосредственно внутри определений scheme_def, sort_def, variant_def,union_def,short_record_def,abbreviation_def,prefix_application,infix_application, single_variable_def, multiple_variable_def, single_channel_def,multiple_channel_def, axiom_naming или id_or_wildcard;id_or_op,встречающихся• идентификатораилиоперациинепосредственно внутри конструктора constructor, деструктораdestructor, реконструктора reconstructor или связывания binding;• идентификатора или операции id_or_op, которые являются внутреннимобразцом inner_pattern.Все остальные вхождения считаются точками использования данногоидентификатора или операции.Каждая точка определения идентификатора или операции является частьюнекоторой декларативной конструкции, представляющей, по крайней мере,определение, с помощью которого задается данный идентификатор илиоперация.Точка использования идентификатора или операции называется видимой,если есть какое-либо видимое определение, с помощью которого задаетсяуказанный идентификатор или операция.87Допустимая точка использования некоторого идентификатора или операцииимеет соответствующее определение (или интерпретацию).
Для любойточки использования идентификатора или операции, возможны три случая:1. Видимого определения, с помощью которого вводится данныйидентификатор или операция, нет, т.е. указанная точка использованияне является видимой. В этом случае точка использования считаетсянедопустимой и, следовательно, данный идентификатор или операцияне имеют соответствующего определения.2. Есть в точности одно видимое определение, с помощью котороговводится данный идентификатор или операция. Это определение иявляется соответствующим определением указанного идентификатораили операции.3.
Есть два или более видимых определений, с помощью которыхвводится данный идентификатор или операция. Согласно правиламвидимости и контекстным условиям для декларативных конструкцийэто возможно только для идентификаторов и операций,представляющихзначения.Вэтомслучаеединственноесоответствующее определение находится (если оно вообще можетбыть найдено) по правилам перегрузки имен. Если невозможно найтиединственное соответствующее определение, то данная точкаиспользования считается недопустимой.Контекст и правила видимости. У всех операций есть одно или болеепредопределенное значение, контекстом которого служит вся спецификацияцеликом и которое не может быть скрыто, поэтому операции всегдаявляются видимыми.Контекстные условия. Точка использования идентификатора или операциидолжна быть видимой, и при этом должно существовать единственноесоответствующее определение данного идентификатора или операции.Отсюда следует, что максимальный тип точки определения операции долженразличаться с максимальным типом (типами) предопределенных значенийданной операции.Атрибуты.Дляидентификатора,представляющегосхему,егомаксимальный класс и возможный формальный параметр схемыопределяются соответствующим определением этого идентификатора (см.раздел 3.2).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
