rsl.formal.specifications.conspect (811084), страница 8
Текст из файла (страница 8)
Выражение function_type_expr задает тип функций, переводящихтип параметра, представленный выражением type_expr, в тип результата,представленный выражением type_expr конструкции result_desc. Описаниядоступа access_desc конструкции result_desc специфицируют, к какимпеременным и каналам может осуществляться доступ при применениифункций. В зависимости от значения метапеременной function_arrow функцииявляются частично вычислимыми или всюду вычислимыми, как описываетсяниже.• Частично вычислимые (partial) функцииВыражение function_type_expr вида:~ opt-access_desc-string type_exprtype_expr1 →2определяет тип частичных функций из типа, представленного первымвыражением type_expr, в тип, представленный вторым выражением40type_expr.
Этот тип содержит функции, удовлетворяющие следующемуограничению: для любой такой функции f и для любого x,принадлежащего максимальному типу первого выражения type_expr,эффект от применения функционального выражения f(x) в любомсостоянии таков, что:- осуществляется только доступ к переменным и каналам,описанным в конструкции opt-access_desc-string;- если вычисление выражения завершается (возможно, послевыполнения ряда взаимодействий), то результирующее значениепринадлежит максимальному типу второго выражения type_expr;- если вычисление выражения представляет сходящийся процесс (isconvergent) и x принадлежит типу, представленному первымвыражением type_expr, то результирующее значение принадлежиттипу, представленному вторым выражением type_expr.• Всюду вычислимые (total) функцииВыражение function_type_expr вида:type_expr → result_descпредставляет собой краткую запись выражения:~ result_desc • ∀ x : type_expr • f(x) post true ⏐}{⏐ f : type_expr →которое обеспечивает, что f и x не являются свободными переменнымивыражений type_expr и result_desc.Это означает, что выражение function_type_expr вида:type_expr1 → opt-access_desc-string type_expr2определяет тип всюду определенных функций из типа,представленного первым выражением type_expr, в тип, представленныйвторым выражением type_expr.
Этот тип содержит те функции,принадлежащие типу:~ opt-access_desc-string type_exprtype_expr1 →2которые удовлетворяют следующему ограничению: для любой такойфункции f и для любого x, принадлежащего типу, представленномупервымвыражениемtype_expr,эффектотпримененияфункционального выражения f(x) в любом состоянии представляетсобой сходящийся процесс.5.9. Подтипы (Subtype Expressions)Синтаксис.subtype_expr ::={⏐ single_typing pure-restriction ⏐}41Контекст и правила видимости.
Контекстом указания типа single_typingявляется ограничение restriction.Контекстные условия. Ограничение restriction должно быть представлятьсобой чистое выражение.Атрибуты. Максимальным типом выражения subtype_expr являетсямаксимальный тип входящего в это выражение указания типа single_typing.Семантика. Выражение subtype_expr представляет подтип типа, заданногоуказанием типа single_typing.
Данный подтип содержит любое значение,сохраняющее истинность ограничения restriction во всех состояниях, при этомвычисление ограничения производится в контексте определений,получаемых путем сопоставления указанного значения со связыванием,также представленным в указании типа single_typing.5.10. Типовое выражение в скобках (Bracketed Type Expressions)Синтаксис.bracketed_type_expr ::=( type_expr )Атрибуты.
Максимальным типом выражения bracketed_type_expr являетсямаксимальный тип входящего в него выражения type_expr.Семантика. Выражение bracketed_type_expr представляет тот же тип, что итиповое выражение type_expr.5.11. Описания доступа (Access Descriptions)Синтаксис.access_desc ::=access_mode access-listaccess_mode ::=read ⏐write ⏐in ⏐outaccess ::=variable_or_channel-name ⏐enumerated_access ⏐completed_access ⏐comprehended_accessenumerated_access ::={ opt-access-list }completed_access ::=any42comprehended_access ::={ access ⏐ pure-set_limitation }Терминология. Описание статического доступа по чтению представляетсобой некоторое множество переменных. Описание статического доступапо записи также представляет собой некоторое множество переменных.Описание статического доступа по вводу так же, как описаниестатического доступа по выводу представляет собой некоторое множествоканалов.Статический доступ – это множество переменных или множество каналов.Контекст и правила видимости.
В конструкции comprehended_accessконтекст ограничения set_limitation расширяется до конструкции access.Контекстные условия. Если значением метапеременной access являетсяимя name, это имя должно представлять:• переменную, если оно появляется в списке access-list описанияaccess_desc со значениями read или write в качестве режима доступаaccess_mode;• канал, если оно появляется в списке access-list описания access_desc созначениями in или out в качестве режима доступа access_mode.Входящее в конструкцию comprehended_access ограничение set_limitationдолжно представлять собой чистое выражение.Атрибуты. С описаниями opt-access_desc-string и access_desc связаны четыреописания статического доступа: описание статического доступа по чтению,описание статического доступа по записи, описание статического доступа повводу и описание статического доступа по выводу.Для пустой строки описания nil-access_desc-string описание статическогодоступа по чтению, записи, вводу и выводу являются пустыми.Для строки access_desc-string описание статического доступа по чтениюпредставляет собой объединение описаний статического доступа по чтениювсех входящих в данную строку описаний access_desc.
Аналогично дляописаний доступа по записи, вводу и выводу.Для описания access_desc с режимом доступа read описание статическогодоступа по чтению равно объединению статических доступов егосоставляющих access, тогда как его описания статического доступа позаписи, вводу и выводу пусты. Аналогично для описания access_desc срежимом доступа in или out. Для описания access_desc с режимом доступаwrite описания статического доступа по чтению и по записи оба равныобъединению статических доступов его составляющих access, тогда как егоописания статического доступа по вводу и выводу пусты.С каждой конструкцией access ассоциируется некоторый статическийдоступ.Для имени name, представляющего собой некоторый идентификатор,статическим доступом является множество, которое содержит в качестве43своего единственного элемента переменную или канал, представленнуюданным идентификатором.Статическим доступом перечисления enumerated_access является пустоемножество в случае отсутствия составляющих его элементов access, впротивном случае статический доступ перечисления представляет собойобъединение статических доступов входящих в него конструкций access.Статическим доступом конструкции completed_access вида any являетсямножество всех переменных или каналов, которые определены в ближайшемобъемлющем данную конструкцию классовом выражении или которыемогли быть определены в любом расширении этого классового выражения.Статическим доступом конструкции comprehended_access являетсястатический доступ входящей в нее конструкции access.Семантика.
Описания доступа access_desc в выражении функциональноготипа ограничивают множество функций, представленное даннымвыражением, путем установления, как и к каким переменным и каналамможет осуществляться доступ.Описания доступа opt-access_desc-string и access_desc представляют четыремножества переменных и каналов:• множество переменных с режимом доступа access_mode равным read,из которых может осуществляться чтение, — множество чтения;• множество переменных с режимом доступа access_mode равным write,в которые может осуществляться запись (т.е.
они могут изменяться засчет присваивания), — множество записи; переменные с режимомдоступа write автоматически имеют режим доступа read;• множество каналов с режимом доступа access_mode равным in, покоторым может осуществляться ввод, — множество ввода;• множество каналов с режимом доступа access_mode равным out, покоторым может осуществляться вывод, — множество вывода.Для пустой строки описания nil-access_desc-string множества чтения, записи,ввода и вывода являются пустыми.Для строки access_desc-string множество чтения представляет собойобъединение множеств чтения всех составляющих ее описаний access_desc.Аналогичное утверждение справедливо для множеств записи, ввода ивывода.Для описания access_desc с режимом доступа read множество чтения равнообъединению множеств всех составляющих его конструкций access, тогдакак его множества записи, ввода и вывода пусты.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
