rsl.formal.specifications.conspect (811084), страница 5
Текст из файла (страница 5)
Если значением метапеременной 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)post_condition opt-pre_condition(m ≤ n)25~ opt-access_desc-string type_exprprefix_op : type_expr1 →2prefix_op id post_condition opt-pre_condition~ opt-access_desc-string type_exprinfix_op : type_expr1 × type_expr2 →3id1 infix_op id2 post_condition opt-pre_condition~ можетПри этом в каждой из указанных форм функциональная стрелка →быть заменена функциональной стрелкой →, и любое из выраженеийфункционального типа может быть заменено именем, которое представляетданный тип согласно определению абревиатуры.Конструкции post_condition и opt-pre_condition могут только статическиобращаться по чтению к тем переменным и каналам, которые указаны вописанияхстатическогодоступаopt-access_desc-string1—opt-access_desc-stringm в первой из вышеприведенных форм и в описанияхстатического доступа opt-access_desc-string в двух последних формах.Контекстно-зависимые расширения.
Неявное определение функцииimplicit_function_def является краткой формой для определения значения иаксиомы, причем конкретный вид этой формы зависит от вида конструкцииformal_function_application.Пусть метафункции maximal и express определены так же, как в предыдущемразделе.Тогдаесливкачествезначенияметапеременнойformal_function_applicationиспользуется id_application с единственнымформальным параметром formal_function_parameter, то неявное определениефункции implicit_function_def вида:value~ opt-access_desc-string type_exprid : type_expr1 × … × type_exprn →n+1id(binding1,…,bindingn) post_condition 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)) post_condition opt-pre_conditionЕслисвязываний binding1,…,bindingn пуст, то выражениеtype_expr1 × … × type_exprn должно быть Unit и использовать квантор ненужно.Здесь так же, как и в случае явного определения функции диапазон значенийкаждого формального параметра bindingi шире максимального типасоответствующего формального параметра type_expri .Аналогичное расширение имеет место, когда в качестве функциональнойстрелки используется символ →.Подобным же образом рассматривается случай, когда конструкцияid_applicationсодержитболееодногоформальногопараметраformal_function_parameter.26списокЕсли в качестве значения метапеременной formal_function_applicationиспользуется prefix_application, то неявное определение функцииimplicit_function_def вида:value~ opt-access_desc-string type_exprprefix_op : type_expr1 →2prefix_op id post_condition opt-pre_conditionявляется краткой формой определений:value~ opt-access_desc-string type_exprprefix_op : type_expr1 →2axiom∀ id : maximal(type_expr1) •prefix_op id post_condition opt-pre_conditionВ данном случае диапазон значений формального параметра id ширемаксимального типа соответствующего формального параметра type_expr1.Аналогичное расширение имеет место для функциональной стрелки →.Если в качестве значения метапеременной formal_function_applicationиспользуетсяinfix_application,тонеявноеопределениефункцииimplicit_function_def вида:value~ opt-access_desc-string type_exprinfix_op : type_expr1 × type_expr2 →3id1 infix_op id2 post_condition 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 post_condition opt-pre_conditionЗдесь каждый формальный параметр idi диапазоном своих значенийпревосходит максимальный тип соответствующего формального параметраtype_expri.Аналогичное расширение справедливо для функциональной стрелки →.3.5.
Объявление переменных (Variable Declarations)Синтаксис:variable_decl ::=variable variable_def-listvariable_def ::=single_variable_def │multiple_variable_def27single_variable_def ::=opt-comment-string id : type_expr opt-initialisationinitialisation ::=:= pure-value_exprmultiple_variable_def ::=opt-comment-string id-list2 : type_exprТерминология.
Переменная – это некая сущность, в которой могутхраниться значения некоторого типа. Присваивание значения переменнойозначает запоминание этого значения в указанной переменной. Значениеможет быть присвоено переменной явно с помощью выраженияприсваивания (см. раздел 6.20).Под состоянием спецификации понимается присваивание значений всемпеременным, определенным в объектах данной спецификации.Определение переменной single_variable_def является циклическим, еслимаксимальный тип выражения type_expr зависит от переменной, которая самазадается этим определением single_variable_def.Максимальный тип зависит от переменной v , если он ссылается на v или налюбую другую переменную или канал, чей максимальный тип зависит от v.Контекстно-независимые расширения.
Множественное определениепеременных multiple_variable_def есть краткая запись двух или болееопределений каждой отдельной переменной, т.е. определение переменныхmultiple_variable_def вида:variable id1, … ,idn : type_exprявляется краткой формой для определений:variableid1 : type_expr,•••idn : type_exprКонтекстные условия.
Все входящие в объявление переменных variable_declопределения переменных variable_def должны быть совместимы.Определение переменной single_variable_def не должно быть циклическим.В инициализации initialisation выражение value_expr должно представлятьсобой чистое выражение, и его максимальный тип должен быть меньше илиравен максимальному типу определяемой переменной.Атрибуты. В определении переменной single_variable_def максимальнымтипом соответствующего id является максимальный тип выражения type_expr.Максимальное определение для определения переменной single_variable_defполучается путем замены входящего в это определение типового выраженияtype_expr на соответствующее выражение для максимального типа иудаления инициализации (если она присутствует).Семантика.
Определение переменной single_variable_def задает конкретныйидентификатор id для некоторой переменной, в которой могут храниться28значения максимального типа для типа, представленного выражениемtype_expr. Типом этой переменной является тип, представленныйвыражением type_expr.В дополнении к этому может быть задано инициализирующее выражение,значение которого представляет собой начальное значение определяемойпеременной.Если инициализация initialisation не задана, начальным значением переменнойсчитается некоторое произвольным образом выбранное значение внутри еетипа.3.6. Объявление каналов (Channel Declarations)Синтаксис:channel_decl ::=channel channel_def-listchannel_def ::=single_channel_def │multiple_channel_defsingle_channel_def ::=opt-comment-string id : type_exprmultiple_channel_def ::=opt-comment-string id-list2 : type_exprТерминология.
Канал – это среда передачи данных, по которой могутвзаимодействовать параллельно выполняющиеся выражения.Для того чтобы два выражения взаимодействовали посредством канала, одноиз них должно передавать данные в этот канал (т.е. использовать его длявывода), в то время как другое должно получать из него данные(использоватьканалдляввода).Взаимодействиеявляетсясинхронизированным: выражение, передающее данные в канал, осуществляетвывод только в том случае, если принимающее выражение одновременноосуществляет ввод данных из этого канала.Определение канала single_channel_def является циклическим, еслимаксимальный тип выражения type_expr зависит от канала, который самзадается тем же определением single_channel_def.Максимальный тип зависит от канала c , если он ссылается на c или налюбой другой канал или переменную, максимальный тип которой зависит отc.Контекстно-независимые расширения. Множественное определениеmultiple_channel_def является сокращенной формой для двух или болееопределений каждого отдельного канала, т.е.
определение каналовmultiple_variable_def вида:channel id1, … ,idn : type_expr29является краткой формой для определений:channelid1 : type_expr,•••idn : type_exprКонтекстные условия. Все входящие в объявление каналов channel_declопределения каналов channel_def должны быть совместимы.Определение канала single_channel_def не должно быть циклическим.Атрибуты. В определении канала single_channel_def максимальным типомсоответствующего id является максимальный тип выражения type_expr.Максимальное определение для определения канала single_channel_defполучается путем замены входящего в это определение типового выраженияtype_expr на соответствующее выражение для максимального типа.Семантика.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
