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

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

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

explicit_function_def ::=

opt-comment-string single_typing

formal_function_application  value_expr opt-pre_condition

formal_function_application ::=

id_application │

prefix_application │

infix_application

id_application ::=

value-id formal_function_parameter-string

formal_function_parameter ::=

( opt-binding-list )

prefix_application ::=

prefix_op id

infix_application ::=

id infix_op id

Терминология. Телом явно определяемой функции является выражение, указанное в определении этой функции.

Контекст и правила видимости. В определении explicit_function_def контекстом конструкции formal_function_application является выражение value_expr и необязательное предусловие opt-pre_condition.

Контекстные условия. Связывание binding в указании типа single_typing должно быть именем или операцией id_or_op (т.е. декартово произведение product_binding не допускается).

Если метапеременная id_or_op в указании типа single_typing является идентификатором id, то в качестве значения метапеременной formal_function_application должна использоваться конструкция id_application этого идентификатора id. Если id_or_op в single_typing является префиксной операцией prefix_op, то в качестве значения метапеременной formal_function_application должна использоваться конструкция prefix_application этой операции prefix_op. И наконец, если id_or_op в single_typing является инфиксной операцией infix_op, то в качестве значения метапеременной formal_function_application должна использоваться конструкция infix_application этой операции infix_op.

Максимальный тип конструкции single_typing должен быть функциональным типом. Если значением метапеременной formal_function_application является infix_application, то параметрическая часть соответствующего функционального типа должна представлять собой декартово произведение двух типов. Если значением метапеременной formal_function_application является id_application, то соответствующий функциональный тип должен быть сформирован с использованием по крайней мере такого количества типов (каждый тип указывается перед функциональной стрелкой или ), сколько формальных параметров formal_function_parameter указано в определении данной функции.

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

id : type_expr₁ opt-access_desc-string₁ type_expr₂

… opt-access_desc-string_n type_expr_n+1

id(opt-binding-list₁)(opt-binding-list₂)…(opt-binding-list_m) 

value_expr opt-pre_condition

prefix_op : type_expr₁ opt-access_desc-string type_expr₂

prefix_op id  value_expr opt-pre_condition

infix_op : type_expr₁  type_expr₂ opt-access_desc-string type_expr₃

id₁ infix_op id₂  value_expr opt-pre_condition

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

В первой из приведенных выше форм максимальный тип выражения value_expr должен быть меньше или равен максимальному типу выражения type_expr_n+1 при m = n или конструкции:

type_expr_m+1 … opt-access_desc-string_n type_expr_n+1

при m  n.

Во второй форме максимальный тип выражения value_expr должен быть меньше или равен максимальному типу выражения type_expr₂.

В третьей форме максимальный тип выражения value_expr должен быть меньше или равен максимальному типу выражения type_expr₃.

Выражение value_expr и предусловие opt-pre_condition могут только статически обращаться к тем переменным и каналам, которые указаны в описаниях статического доступа opt-access_desc-string₁ — opt‑access_desc‑string_m в первой из вышеприведенных форм и в описаниях статического доступа opt‑access_desc‑string в двух последних формах.

Контекстно-зависимые расширения. Определение функции explicit_function_def является краткой формой для определения значения и аксиомы, причем конкретный вид этой формы зависит от вида конструкции formal_function_application.

Пусть метафункция maximal преобразует тип в соответствующий ему максимальный тип, и пусть метафункция express определена так же, как в разделе 3.4.2. Тогда если в качестве значения метапеременной formal_function_application используется id_application с единственным формальным параметром formal_function_parameter, то явное определение функции explicit_function_def вида:

value

id : type_expr₁  …  type_expr_n opt-access_desc-string type_expr_n+1

id(binding₁,…,binding_n)  value_expr opt-pre_condition

где n  1, является краткой формой следующих определений:

value

id : type_expr₁  …  type_expr_n opt-access_desc-string type_expr_n+1

axiom

 binding₁ : maximal(type_expr₁),…, binding_n : maximal(type_expr_n) •

id(express(binding₁),…,express(binding_n))  value_expr opt-pre_condition

При этом если список связываний binding₁,…,binding_n пуст, то выражение type_expr₁  …  type_expr_n должно быть Unit и использовать квантор не нужно.

Заметим, что диапазон значений каждого формального параметра binding_i шире максимального типа соответствующего формального параметра type_expr_i .

Аналогичное расширение имеет место, если функциональную стрелку заменить функциональной стрелкой .

Подобным же образом рассматривается случай, когда конструкция id_application содержит более одного формального параметра formal_function_parameter.

Если в качестве значения метапеременной formal_function_application используется prefix_application, то явное определение функции explicit_function_def вида:

value

prefix_op : type_expr₁ opt-access_desc-string type_expr₂

prefix_op id  value_expr opt-pre_condition

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

value

prefix_op : type_expr₁ opt-access_desc-string type_expr₂

axiom

 id : maximal(type_expr₁) •

prefix_op id  value_expr opt-pre_condition

В данном случае следует обратить внимание на то, что формальный параметр id диапазоном своих значений превосходит максимальный тип соответствующего формального параметра type_expr₁.

Аналогичное расширение справедливо, если в качестве функциональной стрелки используется символ .

Если в качестве значения метапеременной formal_function_application используется infix_application, то явное определение функции explicit_function_def вида:

value

infix_op : type_expr₁  type_expr₂ opt-access_desc-string type_expr₃

id₁ infix_op id₂  value_expr opt-pre_condition

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

value

infix_op : type_expr₁  type_expr₂ opt-access_desc-string type_expr₃

axiom

 id₁ : maximal(type_expr₁),id₂ : maximal(type_expr₂)•

id₁ infix_op id₂  value_expr opt-pre_condition

Здесь также каждый формальный параметр id_i диапазоном своих значений превосходит максимальный тип соответствующего формального параметра type_expr_i.

Аналогичное расширение имеет место для случая функциональной стрелки .

3.4.5. Неявное определение функций (Implicit Function Definitions)

Синтаксис:

implicit_function_def ::=

opt-comment-string single_typing formal_function_application

post_condition opt-pre_condition

Контекст и правила видимости. В определении implicit_function_def контекстом конструкции formal_function_application является постусловие post_condition и необязательное предусловие opt-pre_condition.

Контекстные условия. Связывание binding в указании типа single_typing должно быть идентификатором или операцией id_or_op (т.е. декартово произведение product_binding не допускается).

Если метапеременная id_or_op в конструкции single_typing является идентификатором id, то в качестве значения метапеременной formal_function_application должно использоваться id_application этого идентификатора id. Если id_or_op в single_typing является префиксной операцией prefix_op, то в качестве значения метапеременной formal_function_application должно использоваться prefix_application этой операции prefix_op. И наконец, если id_or_op в single_typing является инфиксной операцией infix_op, то значением метапеременной formal_function_application должно быть infix_application этой операции infix_op.

Максимальным типом конструкции single_typing должен быть функциональный тип. Если значением метапеременной formal_function_application является infix_application, то параметрическая часть функционального типа должна представлять собой декартово произведение двух типов. Если значением метапеременной formal_function_application является id_application, то функциональный тип должен быть сформирован с использованием по крайней мере такого количества типов (все эти типы указываются перед функциональной стрелкой или ), сколько формальных параметров formal_function_parameter указано в определении данной функции.

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

id : type_expr₁ opt-access_desc-string₁ type_expr₂

… opt-access_desc-string_n type_expr_n+1

id(opt-binding-list₁)(opt-binding-list₂)…(opt-binding-list_m)

post_condition opt-pre_condition (m  n)

prefix_op : type_expr₁ opt-access_desc-string type_expr₂

prefix_op id post_condition opt-pre_condition

infix_op : type_expr₁  type_expr₂ opt-access_desc-string type_expr₃

id₁ infix_op id₂ post_condition opt-pre_condition

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

Конструкции post_condition и opt-pre_condition могут только статически обращаться по чтению к тем переменным и каналам, которые указаны в описаниях статического доступа opt‑access_desc-string₁ — opt‑access_desc‑string_m в первой из вышеприведенных форм и в описаниях статического доступа opt‑access_desc‑string в двух последних формах.

Контекстно-зависимые расширения. Неявное определение функции implicit_function_def является краткой формой для определения значения и аксиомы, причем конкретный вид этой формы зависит от вида конструкции formal_function_application.

Пусть метафункции maximal и express определены так же, как в предыдущем разделе. Тогда если в качестве значения метапеременной formal_function_application используется id_application с единственным формальным параметром formal_function_parameter, то неявное определение функции implicit_function_def вида:

value

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

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