rsl.formal.specifications.conspect (811084), страница 4
Текст из файла (страница 4)
Определение сокращенной записи (Short Record Definitions)Синтаксис:short_record_def ::=opt-comment-string id :: component_kind-stringКонтекстно-независимые расширения. Определение short_record_defявляется краткой формой для определения вариантов с единственнымвариантом, включающим конструктор. Определение short_record_def вида:type id :: component_kind1 … component-kindnпредставляет собой сокращенную запись определения:type id == mk_id(component_kind1, … ,component-kindn)где mk_id задает конструктор данного варианта.3.3.5.
Определение абревиатур (Abbreviation Definitions)Синтаксис:abbreviation_def ::=opt-comment-string id = type_expr19Терминология. Определение abbreviation_def является циклическим, еслимаксимальный тип задающего его тип выражения type_expr зависит от типа,который сам задается посредством этого же определения abbreviation_def.Максимальный тип зависит от некоторого типа t, если он использует этоттип t.Контекстные условия. Определение abbreviation_def не должно бытьциклическим.Атрибуты. Максимальным типом входящего в определение идентификатораid является максимальный тип указанного в этом определении type_expr.Максимальное определение для определения abbreviation_def получаетсяпутем замещения входящего в него типового выражения type_exprсоответствующим выражением для максимального типа.Семантика.
Определение abbreviation_def задает конкретное имя id для типа,представленного выражением type_expr.3.4. Объявление функций (Value Declarations)В языке RSL константа рассматривается как частный случай функции,поэтому для объявления констант и функций предусмотрен единый разделvalue declarations.Синтаксис.value_decl ::=value value_def-listvalue_def ::=commented_typing │explicit_value_def │implicit_value_def │explicit_function_def │implicit_function_def │Контекстные условия. Входящие в объявление value_decl определенияvalue_def должны быть совместимы.3.4.1.
Прокомментированное указание типа (Commented Typing)См. раздел 8.3.4.2. Явное определение констант (Explicit Value Definitions)Синтаксис:explicit_value_def ::=opt-comment-string single_typing = pure-value_exprКонтекстные условия. Максимальный тип выражения value_expr долженбыть меньше или равен максимального типа конструкции single_typing.20Выражение value_expr должно представлять собой чистое выражение (см.раздел 6.1).Контекстно-зависимые расширения.
Явное определение константыexplicit_value_def является краткой формой для определения константы иаксиомы.Пусть метафункция express преобразует связывание (binding) в выражениепутем взятия в скобки всех операций, оставляя остальную часть связываниябез изменения. Семантика операций в скобках описана в разделе 10.3. Тогдаявное определение константы explicit_value_def вида:value binding : type_expr = value_exprявляется сокращением следующего фрагмента:value binding : type_expraxiom express(binding) = value_expr3.4.3. Неявное определение констант (Implicit Value Definitions)Синтаксис:implicit_value_def ::=opt-comment-string single_typing pure-restrictionКонтекстные условия.
Ограничение restriction должно представлять собойчистое выражение.Контекстно-зависимые расширения. Неявное определение константыimplicit_value_def является краткой формой для определения константы иаксиомы.Неявное определение константы implicit_value_def вида:value binding : type_expr • value_exprявляется краткой формой записи следующего фрагмента:value binding : type_expraxiom value_expr3.4.4. Явное определение функций (Explicit Function Definitions)Синтаксис:explicit_function_def ::=opt-comment-string single_typingformal_function_application ≡ value_expr opt-pre_conditionformal_function_application ::=id_application │prefix_application │infix_application21id_application ::=value-id formal_function_parameter-stringformal_function_parameter ::=( opt-binding-list )prefix_application ::=prefix_op idinfix_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 указано вопределении данной функции.Это означает, что существуют следующие три допустимые формы явногоопределения функции:~ opt-access_desc-string type_exprid : type_expr1 →12~ opt-access_desc-string type_expr… →nn+1id(opt-binding-list1)(opt-binding-list2)…(opt-binding-listm) ≡value_expr opt-pre_condition22~ opt-access_desc-string type_exprprefix_op : type_expr1 →2prefix_op id ≡ value_expr opt-pre_condition~ opt-access_desc-string type_exprinfix_op : type_expr1 × type_expr2 →3id1 infix_op id2 ≡ value_expr opt-pre_condition~ можетПри этом в каждой из указанных форм функциональная стрелка →быть заменена функциональной стрелкой →, и любое выражениефункционального типа может быть заменено именем, представляющимданный тип согласно определению абревиатуры.В первой из приведенных выше форм максимальный тип выраженияvalue_expr должен быть меньше или равен максимальному типу выраженияtype_exprn+1 при m = n или конструкции:~ opt-access_desc-string type_exprtype_exprm+1 … →nn+1при m < n.Во второй форме максимальный тип выражения value_expr должен бытьменьше или равен максимальному типу выражения type_expr2.В третьей форме максимальный тип выражения value_expr должен бытьменьше или равен максимальному типу выражения type_expr3.Выражение value_expr и предусловие opt-pre_condition могут толькостатически обращаться к тем переменным и каналам, которые указаны вописанияхстатическогодоступаopt-access_desc-string1—opt-access_desc-stringm в первой из вышеприведенных форм и в описанияхстатического доступа 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~ opt-access_desc-string type_exprid : type_expr1 × … × type_exprn →n+1id(binding1,…,bindingn) ≡ value_expr opt-pre_conditionгде n ≥ 1, является краткой формой следующих определений:value~ opt-access_desc-string type_exprid : type_expr1 × … × type_exprn →n+1axiom∀ binding1 : maximal(type_expr1),…, bindingn : maximal(type_exprn) •id(express(binding1),…,express(bindingn)) ≡ value_expr opt-pre_condition23При этом если список связываний binding1,…,bindingn пуст, то выражениеtype_expr1 × … × type_exprn должно быть Unit и использовать квантор ненужно.Заметим, что диапазон значений каждого формального параметра bindingiшире максимального типа соответствующего формального параметраtype_expri .~Аналогичное расширение имеет место, если функциональную стрелку →заменить функциональной стрелкой →.Подобным же образом рассматривается случай, когда конструкцияid_applicationсодержитболееодногоформальногопараметраformal_function_parameter.Если в качестве значения метапеременной formal_function_applicationиспользуетсяprefix_application,тоявноеопределениефункцииexplicit_function_def вида:value~ opt-access_desc-string type_exprprefix_op : type_expr1 →2prefix_op id ≡ value_expr opt-pre_conditionявляется краткой формой для определений:value~ opt-access_desc-string type_exprprefix_op : type_expr1 →2axiom∀ id : maximal(type_expr1) •prefix_op id ≡ value_expr opt-pre_conditionВ данном случае следует обратить внимание на то, что формальныйпараметр id диапазоном своих значений превосходит максимальный типсоответствующего формального параметра type_expr1.Аналогичное расширение справедливо, если в качестве функциональнойстрелки используется символ →.Если в качестве значения метапеременной formal_function_applicationиспользуетсяinfix_application,тоявноеопределениефункцииexplicit_function_def вида:value~ opt-access_desc-string type_exprinfix_op : type_expr1 × type_expr2 →3id1 infix_op id2 ≡ value_expr opt-pre_conditionявляется краткой формой для следующего фрагмента определений:value~ opt-access_desc-string type_exprinfix_op : type_expr1 × type_expr2 →3axiom∀ id1 : maximal(type_expr1),id2 : maximal(type_expr2)•id1 infix_op id2 ≡ value_expr opt-pre_condition24Здесь также каждый формальный параметр idi диапазоном своих значенийпревосходит максимальный тип соответствующего формального параметраtype_expri.Аналогичное расширение имеет место для случая функциональной стрелки→.3.4.5.
Неявное определение функций (Implicit Function Definitions)Синтаксис:implicit_function_def ::=opt-comment-string single_typing formal_function_applicationpost_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, то параметрическая частьфункционального типа должна представлять собой декартово произведениедвух типов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
