Языки и методы формальной спецификации (1158803), страница 13
Текст из файла (страница 13)
Синтаксис.
assignment_expr ::=
variable-name := value_expr
Контекстные условия. Имя name должно представлять некоторую переменную.
Максимальный тип выражения value_expr должен быть меньше или равен максимального типа имени name.
Атрибуты. Максимальным типом выражения присваивания assignment_expr является Unit.
Выражение присваивания assignment_expr статически производит запись в переменную, представленную входящим в его состав именем name, а также статически производит доступ к переменным или каналам, к которым статически обращается выражение value_expr.
Семантика. Результирующее воздействие выражения присваивания assignment_expr состоит в том, чтобы записать (присвоить) значение выражения value_expr в переменную, представленную именем name. Значением, возвращаемым выражением присваивания assignment_expr, является Unit значение.
6.21. Input-выражения (Input Expressions)
Синтаксис.
input_expr ::=
channel-name ?
Контекстные условия. Имя name должно представлять некоторый канал.
Атрибуты. Максимальным типом input-выражения input_expr является максимальный тип входящего в его состав имени name.
Выражение input_expr статически производит ввод по каналу, представленному именем name, и не обращается статически ни к каким переменным.
Семантика. Результирующее воздействие выражения input_expr состоит в том, чтобы предложить ввести данные по каналу, представленному указанным именем name. Значением, возвращаемым выражением input_expr, является значение, введенное по указанному каналу, в случае, если предложение произвести ввод совпадет с параллельным предложением произвести вывод по тому же каналу.
6.22. Output-выражения (Output Expressions)
Синтаксис.
output_expr ::=
channel-name ! value_expr
Контекстные условия. Имя name должно представлять некоторый канал.
Максимальный тип выражения value_expr должен быть меньше или равен максимального типа имени name.
Атрибуты. Максимальным типом output-выражения output_expr является Unit.
Выражение output_expr статически производит вывод по каналу, представленному входящим в его состав именем name, а также статически обращается к переменным или каналам, к которым статически производит доступ выражение value_expr.
Семантика. Результирующее воздействие выражения output_expr состоит в том, чтобы предложить вывести данные по каналу, представленному указанным именем name. Предлагаемым для вывода значением является значение, возвращаемое выражением value_expr. Выражение output_expr возвращает Unit значение в случае, если предложение произвести вывод совпадет с параллельным предложением произвести ввод по тому же каналу.
6.23. Составные выражения (Structured Expressions)
Синтаксис.
structured_expr ::=
local_expr ½
let_expr ½
if_expr ½
case_expr ½
while_expr ½
until_expr ½
for_expr
6.23.1. Локальные выражения (Local Expressions)
Синтаксис.
local_expr ::=
local opt-decl-string in value_expr end
Контекст и правила видимости. Контекстом объявления opt-decl-string является само это объявление opt-decl-string и выражение value_expr. Это означает, что порядок определений в объявлении 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 end
let_def ::=
typing ½
explicit_let ½
implicit_let
explicit_let ::=
let_binding = value_expr
implicit_let ::=
single_typing restriction
let_binding ::=
binding ½
record_pattern ½
list_pattern
Контекстно-независимые расширения. Выражение let_expr, содержащее в себе более одного определения let_def, является сокращенной формой записи для некоторого числа вложенных let-выражений с единственным определением. То есть выражение let_expr вида:
let let_def1, …, let_defn in value_expr end
является сокращенной формой записи следующего выражения:
let let_def1 in
let let_defn in value_expr end
end
Контекст и правила видимости. В выражении 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 представляет некоторое подмножество моделей, которые удовлетворяют определениям, заданных указанием типа 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 then
value_expr
opt-elsif_branch-string
opt-else_branch
end
elsif_branch ::=
elsif logical-value_expr then value_expr
else_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_branch
end
является сокращенной формой записи выражения:
if value_expr1 then value_expr1 else
if value_expr2 then value_expr2¢ else
if value_exprn then value_exprn¢ opt-else_branch end
end
end
Выражение 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 end
case_branch ::=
pattern value_expr
Контекст и правила видимости. В ветви case_branch контекстом образца pattern является выражение value_expr.
Контекстные условия. В выражении case_expr максимальные типы выражений value_expr, содержащихся в ветвях case_branch, должны иметь наименьшую верхнюю границу.
Атрибуты. Максимальным типом case-выражения case_expr является наименьшая верхняя граница максимальных типов выражений value_expr в соответствующих ветвях case_branch.
В выражении case_expr максимальным контекстным типом образцов pattern в ветвях case_branch является максимальный тип выражения value_expr.
Выражение case_expr статически производит доступ к тем переменным и каналам, к которым статически обращаются содержащиеся в нем выражение value_expr и ветви case_branch.
Ветвь case_branch статически производит доступ к тем переменным и каналам, к которым статически обращается входящее в ее состав выражение value_expr.
Семантика. Результирующее воздействие выражения case_expr состоит в том, чтобы вычислить выражение value_expr, определить соответствующую ветвь case_branch и затем вычислить выражение value_expr, содержащееся в этой ветви. Выражение value_expr вычисляется и возвращает некоторое значение — тестовое значение. Затем просматриваются слева направо ветви case_branch до тех пор, пока данное тестовое значение не совпадет с каким-либо образцом pattern. Такое успешное сопоставление образца с тестовым значением дает в результате некоторый набор определений. В завершении в контексте этих определений вычисляется соответствующее выражение value_expr, содержащееся в ветви case_branch, на которой произошло отождествление образца и тестового значения.