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

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

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

Если ни на одной ветви 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 возвращает значение true. Значением, возвращаемым выражением while_expr, является Unit значение.

Имеет место следующая эквивалентность:

while value_expr₁ do value_expr₂ end



if value_expr₁ then

value_expr₂ ; while value_expr₁ do value_expr₂ end

else skip end

6.23.6. Until-выражения (Until Expressions)

Синтаксис.

until_expr ::=

do unit-value_expr until logical-value_expr end

Контекстно-независимые расширения. Выражение until_expr вида:

do value_expr₁ until value_expr₂ end

представляет собой краткую форму записи выражения:

value_expr₁ ; while  value_expr₂ do value_expr₁ end

6.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 end

1. Связывания (Bindings)

Синтаксис.

binding ::=

id_or_op ½

product_binding

product_binding ::=

( binding-list2 )

Терминология. Значение может быть сопоставлено со связыванием 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 вида (binding₁,…, binding_n) , контекстный тип которой имеет вид t₁ ´ … ´ t_n, максимальными контекстными типами связываний binding₁,…, binding_n являются типы t₁, …, t_n соответственно.

Семантика. Совпадение некоторого значения v максимального контекстного типа t со связыванием binding вида id_or_op дает следующее определение:

id_or_op : t = v

Совпадение значения некоторого декартова произведения (v₁,…,v_n) максимального контекстного типа t₁ ´ … ´ t_n со связыванием product_binding вида (binding₁,…, binding_n) дает набор определений, полученных при совпадении каждого значения v_i максимального контекстного типа t_i со связыванием binding_i.

1. Указания типа (Typings)

Синтаксис.

typing ::=

single_typing ½

multiple_typing

single_typing ::=

binding : type_expr

multiple_typing ::=

binding-list2 : type_expr

commented_typing ::=

opt-comment-string typing

Контекстно-независимые расширения. Все множественные указания типа multiple_typing и typing-list являются сокращенной формой для единичных указаний типа. Так, множественное указание типа multiple_typing вида:

binding₁,…, binding_n : type_expr

является сокращенной формой следующей записи:

(binding₁,…, binding_n) : type_expr ´ … ´ type_expr

где декартово произведение типов имеет длину n.

Список typing-list вида:

binding₁ : type_expr₁,…, binding_n : type_expr_n

является сокращенной формой следующей записи:

(binding₁,…, binding_n) : type_expr₁ ´ … ´ type_expr_n

Разложение на единичные указания типа списка 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 вида:

(binding₁,…, binding_n) : type_expr₁ ´ … ´ type_expr_n

представляет набор определений, представленных каждым единичным указанием типа:

binding₁ : type_expr₁







binding_n : type_expr_n

1. 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) в противном случае.

• Если неявное приведение типов является композицией функций f₁…f_n (n  2), то образец pattern или внутренний образец inner_pattern p представляет собой сокращенную форму образца записи record_pattern f₁(…(f_n(= p))…), если p является именем name, и f₁(…(f_n(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.

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

9.5. Образцы декартовы произведения (Product Patterns)

Синтаксис.

product_pattern ::=

( inner_pattern-list2 )

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

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

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

Семантика.

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

(inner_pattern₁,…, inner_pattern_n)

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

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