Языки и методы формальной спецификации (1158803), страница 15

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 15)

тогда тестовое значение должно быть декартовым произведением вида (v₁,…,v_n) и в дополнении к этому каждое значение v_i должно сопоставляться с соответствующим внутренним образцом inner_pattern_i.

• Результирующие определения: набор определений, получаемый путем сопоставления каждого значения v_i с внутренним образцом inner_pattern_i.

9.6. Образцы записи (Record Patterns)

Синтаксис.

record_pattern ::=

pure_value-name ( inner_pattern-list )

Контекстные условия. В образце записи record_pattern имя name должно представлять некоторое значение и его максимальный тип должен быть типом чистой функции. Тип результирующей части этого функционального типа должен быть меньше или равен максимального контекстного типа данного образца записи record_pattern. Кроме того, если образец запись record_pattern имеет вид:

name(inner_pattern₁,…, inner_pattern_n) ( n  1 )

то параметрическая часть данного функционального типа должна иметь вид t₁ ´ … ´ t_n.

В образце записи record_pattern составляющие его внутренние образцы inner_pattern должны быть совместимы.

Атрибуты. В образце записи record_pattern вида name(inner_pattern) максимальным контекстным типом внутреннего образца inner_pattern является параметрическая часть максимального типа указанного имени name.

В образце записи record_pattern вида name(inner_pattern₁,…, inner_pattern_n) максимальными контекстными типами внутренних образцов inner_pattern₁,…, inner_pattern_n являются типы t₁, …, t_n соответственно, где тип параметрической части максимального типа имени name имеет вид t₁ ´ … ´ t_n.

Семантика.

• Успешное сопоставление: пусть образец запись record_pattern имеет вид:

name(inner_pattern₁,…, inner_pattern_n) ( n  1 )

и пусть v — тестовое значение, тогда должны существовать значения v₁,…,v_n такие, что:

v = name(v₁,…, v_n)

и в дополнении к этому каждое значение v_i должно сопоставляться с соответствующим внутренним образцом inner_pattern_i.

• Результирующие определения: набор определений, получаемый путем сопоставления каждого значения v_i с внутренним образцом inner_pattern_i, при этом значения v₁,…,v_n недетерминированно выбираются таким образом, чтобы были выполнены условия успешного совпадения, описанные выше.

9.7. Образцы списки (List Patterns)

Синтаксис.

list_pattern ::=

enumerated_list_pattern 

concatenated_list_pattern

Контекстные условия. Максимальным контекстным типом образца списка list_pattern должен быть какой-либо списочный тип.

9.7.1. Образцы списки, заданные перечислением (Enumerated List Patterns)

Синтаксис.

enumerated_list_pattern ::=

 opt-inner_pattern-list 

Контекстные условия. Составляющие данную конструкцию внутренние образцы inner_pattern должны быть совместимы.

Атрибуты. Максимальным контекстным типом каждого внутреннего образца inner_pattern является тип элемента максимального контекстного типа содержащего их образца списка list_pattern.

Семантика.

• Успешное сопоставление: пусть образец список enumerated_list_pattern имеет вид:

inner_pattern₁,…, inner_pattern_n ( n  0 )

тогда тестовое значение должно представлять собой список вида v₁,…,v_n и в дополнении к этому каждое значение v_i должно сопоставляться с соответствующим внутренним образцом inner_pattern_i.

• Результирующие определения: набор определений, получаемый путем сопоставления каждого значения v_i с внутренним образцом inner_pattern_i.

9.7.2. Образцы списки, заданные конкатенацией (Concatenated List Patterns)

Синтаксис.

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

тогда тестовое значение должно представлять собой список вида l₁ ^ l₂, где l₁ сопоставляется с образцом списком enumerated_list_pattern и l₂ сопоставляться с внутренним образцом inner_pattern.

• Результирующие определения: набор определений, получаемый путем сопоставления списка l₁ с образцом списком enumerated_list_pattern и списка l₂ с внутренним образцом inner_pattern.

9.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 = v

9.8.2. Образцы равенства (Equality Patterns)

Синтаксис.

equality_pattern ::=

= pure_value-name

Контекстные условия. В образце равенстве equality_pattern имя name должно представлять некоторое значение.

Максимальный тип этого имени name (см. раздел 10) должен быть меньше или равен максимального контекстного типа содержащего его образца равенства equality_pattern.

Семантика.

• Успешное сопоставление: значение, представленное именем name, должно быть равно тестовому значению.

• Результирующие определения: нет.

1. Имена

10.1. Общие замечания

Синтаксис.

name ::=

id 

( op )

Атрибуты. Если имя name представляет некоторую схему, то для него определен максимальный класс, т.е. максимальный класс ассоциируемого с данным именем классового выражения. В случае параметризованной схемы у этого имени есть также некоторый формальный параметр схемы. Если имя name представляет какой-либо тип, значение, переменную или канал, то с ним (с именем) ассоциируется некоторый максимальный тип. Ниже для каждой из указанных альтернатив определены свои конкретные атрибуты.

Семантика. Имя name представляет некоторую сущность, которая является схемой, типом, значением, переменной или каналом.

10.2. Идентификаторы (Identifiers)

Атрибуты. Если имя name представляет собой идентификатор id, то его атрибутами являются атрибуты данного идентификатора id.

Семантика. Идентификатор id представляет сущность, с которой он связан соответствующим определением.

10.3. Операции (Operators)

Контекст и правила видимости. В конструкции name, являющейся операцией op, видны все предопределенные значения операций.

Атрибуты. Максимальным типом имени name, представляющим собой операцию, является максимальный тип этой операции op.

Семантика. Операция op представляет сущность, с которой она связана соответствующим определением.

Скобки превращают операцию op в функцию, которую можно применять в префиксной нотации как аппликативное выражение (см. раздел 6.10). С учетом того, что операция op может быть префиксной prefix_op или инфиксной infix_op, это означает выполнение следующих эквивалентностей:

prefix_op value_expr  (prefix_op )( value_expr )

value_expr₁ infix_op value_expr₂  (infix_op )( value_expr₁, value_expr₂ )

1. Идентификаторы и операции

11.1. Общие замечания

Синтаксис.

id_or_op ::=

id 

op

op ::=

infix_op ½

prefix_op

Терминология. Любое встречающееся в тексте вхождение идентификатора или операции (id_or_op, id или op) может быть связано либо с их определением — точка определения (defining occurrence), либо с их применением или использованием — точка использования (applied occurrence).

Точками определения считаются следующие вхождения:

• идентификатора (идентификаторов) 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.

Все остальные вхождения считаются точками использования данного идентификатора или операции.

Каждая точка определения идентификатора или операции является частью некоторой декларативной конструкции, представляющей, по крайней мере, определение, с помощью которого задается данный идентификатор или операция.

Точка использования идентификатора или операции называется видимой, если есть какое-либо видимое определение, с помощью которого задается указанный идентификатор или операция.

Допустимая точка использования некоторого идентификатора или операции имеет соответствующее определение (или интерпретацию). Для любой точки использования идентификатора или операции, возможны три случая:

1. Видимого определения, с помощью которого вводится данный идентификатор или операция, нет, т.е. указанная точка использования не является видимой. В этом случае точка использования считается недопустимой и, следовательно, данный идентификатор или операция не имеют соответствующего определения.

2. Есть в точности одно видимое определение, с помощью которого вводится данный идентификатор или операция. Это определение и является соответствующим определением указанного идентификатора или операции.

3. Есть два или более видимых определений, с помощью которых вводится данный идентификатор или операция. Согласно правилам видимости и контекстным условиям для декларативных конструкций это возможно только для идентификаторов и операций, представляющих значения. В этом случае единственное соответствующее определение находится (если оно вообще может быть найдено) по правилам перегрузки имен. Если невозможно найти единственное соответствующее определение, то данная точка использования считается недопустимой.

Контекст и правила видимости. У всех операций есть одно или более предопределенное значение, контекстом которого служит вся спецификация целиком и которое не может быть скрыто, поэтому операции всегда являются видимыми.

Контекстные условия. Точка использования идентификатора или операции должна быть видимой, и при этом должно существовать единственное соответствующее определение данного идентификатора или операции. Отсюда следует, что максимальный тип точки определения операции должен различаться с максимальным типом (типами) предопределенных значений данной операции.

Характеристики

Список файлов книги