rsl.formal.specifications.conspect (811084), страница 7
Текст из файла (страница 7)
любым типом, состоящим излитералов, за исключением Nat и Text).• именем, соответствующее определение которого представляет собойопределение абстрактного типа, варианта, объединения илисокращенной записи.• именем,соответствующееопределениекоторогоявляетсяопределением аббревиатуры, в состав которого входит максимальноетиповое выражение.• типовым выражением, построенным из максимальных типовыхвыражений и описаний статического доступа путем применения~ или ⎯⎯→ (т.е. любыходного из типовых операторов × , -infset, ω, →m*типовых операторов за исключением -set, и →).• выражением для задания подтипа, если входящее в его состав типовоевыражение является максимальным и ограничение, с помощьюкоторого задается подтип, сохраняется для всех значений этого(максимального) типа, представленного данным максимальнымтиповым выражением.• заключенным в скобки типовым выражением, где указанное в скобкахтиповое выражение является максимальным.Два максимальных типа считаются неразличимыми тогда и только тогда,когда существуют два типовых выражения, представляющие эти типы иразличающиеся не больше, чем описаниями статического доступасодержащихся в них функциональных типов.Два максимальных типа считаются различимыми тогда и только тогда, когдаони не являются неразличимыми.Использование в спецификации определений объединений (union definitions)вызывает потенциальное приведение типов, которое является частичнойфункцией между максимальными типами.Будем говорить, что имеет место потенциальное приведение (potentialcoercion) максимального типа t1 к максимальному типу t2 тогда и толькотогда, когда выполняются следующие условия:1.
t1 идентичен с t2, в этом случае потенциальное приведение типа t1 к t2представляет собой тождественную функцию.2. задано определение объединения вида:id2 = … ⏐ id1 ⏐ …в котором id1 имеет максимальный тип t1 и id2 имеет максимальный типt2, в этом случае потенциальное приведение типа t1 к типу t2представляет собой функцию id2_from_id1.3. заданы типы t11, t12, t21, t22 и описание статического доступаopt-access_desc-string такие, что имеется потенциальное приведение35типов t11 к t21 и t12 к t22, кроме того, типы t1 и t2 построены одним изперечисленных ниже способов.
В этом случае потенциальноеприведение типа t1 к типу t2 выводится из других потенциальныхприведений очевидным образом.(a)(b)(c)(d)(e)t1 есть …× t11 × … и t2 есть … × t21 × …t1 есть t11–infset и t2 есть t21-infset.t1 есть t11ω и t2 есть t21ω.t1 есть t11 ⎯⎯m→ t12 и t2 есть t21 ⎯⎯m→ t22.~ opt-access_desc-string t иt1 есть t11 →12~ opt-access_desc-string t .t2 есть t21 →224. задан тип t3 такой, что f13 является потенциальным приведением типа t1к t3 и f32 соответствующим приведением t3 к t2; в этом случаепотенциальным приведением типа t1 к t2 является f32 ° f13.Максимальный тип t1 называется приводимым к максимальному типу t2, еслисуществует одно и только одно потенциальное приведение типа t1 к t2.Максимальный тип t1 меньше или равен максимального типа t2, если онприводим к подтипу типа t2.Максимальный тип t называется верхней границей набора максимальныхтипов, если все максимальные типы данного набора меньше или равны t.Максимальный тип называется наименьшей верхней границей наборамаксимальных типов, если он является верхней границей данного набора именьше или равен всех остальных верхних границ этого набора.Атрибуты.
С любым типовым выражением type_expr ассоциируетсянекоторый максимальный тип. Тип, представленный типовым выражениемtype_expr, является подтипом ассоциируемого с ним максимального типа. Вниже следующих разделах для каждого конкретного случая типовоговыражения определяется соответствующий максимальный тип.Семантика. Типовое выражение type_expr представляет некоторый тип.Конкретные типы для каждой разновидности типовых выраженийопределяются в следующих разделах.5.2.
Предопределенные типы (Type Literals)Синтаксис.type_literal ::=Unit ⏐Bool ⏐Int ⏐Nat ⏐Real ⏐Text ⏐Char36Атрибуты. Максимальным типом Unit является Unit.Максимальным типом Bool является Bool.Максимальным типом Int является Int.Максимальным типом Nat является Int.Максимальным типом Real является Real.Максимальным типом Text является Charω.Максимальным типом Char является Char.Семантика. Тип type_literal представляет предопределенный тип.Тип Unit имеет единственное значение ().Значениями типа Bool являются булевские константы true и false.Значениями типа Int являются целые числа (…, -2, -1, 0, 1, 2, …).Литерал Nat является сокращенной записью выражения, задающегоследующий подтип {⏐ i : Int • i ≥ 0 ⏐}.Значениями типа Real являются вещественные числа (…, -4.3, …, 12.23, …).Значениями типа Char являются ASCII символы в одинарных кавычках ('a','b', …).Литерал Text является сокращенной записью типового выражения Char*.5.3.
Имена (Names)Контекстные условия. В типовом выражении type_expr, являющимсяименем name, это имя name должно представлять некоторый тип.Атрибуты и семантика описаны в разделе 10.5.4. Декартово произведение типов (Product type expressions)Синтаксис.product_type_expr ::=type_expr-product2Терминология. Декартово произведение – это значение вида (v1,…,vn).Длиной декартова поризведения типов product_type_expr называетсяколичество составляющих его типовых выражений type_expr.Атрибуты. Максимальным типом выражения product_type_expr видаtype_expr1 × … × type_exprn является декартово произведение t1 × … × tn, где t1,…, tn являются максимальными типами соответственно выраженийtype_expr1, …, type_exprn.Семантика. Декартово произведение типов product_type_expr видаtype_expr1 × … × type_exprn представляет тип всех декартовых произведенийвида (v1,…,vn), где тип каждого vi представлен выражением type_expri.375.5. Множественные типы (Set type expressions)Синтаксис.set_type_expr ::=finite_set_type_expr ⏐infinite_set_type_exprfinite_set_type_expr ::=type_expr-setinfinite_set_type_expr ::=type_expr-infsetТерминология.
Множество – это, возможно, пустой неупорядоченныйнабор различных значений одного и того же типа.Атрибуты. Максимальным типом выражения set_type_expr вида type_expr-setили type_expr-infset является t-infset , где t представляет собой максимальныйтип выражения type_expr.Семантика. Множественный тип, определяемый типовым выражениемset_type_expr, представляет тип из подмножеств множества значений, типкоторых представлен входящим в это выражение type_expr. Если в качестветипового оператора используется -set, то данный тип содержит все конечныеподмножества. Если типовым оператором является -infset, тосоответствующий множественный тип содержит все (конечные ибесконечные) подмножества.Множество характеризуется своими элементами.5.6.
Типы списки (List type expressions)Синтаксис.list_type_expr ::=finite_list_type_expr ⏐infinite_list_type_exprfinite_list_type_expr ::=type_expr*infinite_list_type_expr ::=type_exprωТерминология. Список – это, возможно, пустая последовательностьзначений одного и того же типа, допускающая повторения элементов.Атрибуты. Максимальным типом выражения list_type_expr вида type_expr*или type_exprω является tω, где t представляет собой максимальный типвыражения type_expr.Семантика. Выражение list_type_expr представляет тип списков значений,тип которых определяется входящим в это выражение type_expr.
Если в38качестве типового оператора используется *, то данный тип содержит всеконечные списки. Если типовым оператором является ω, то соответствующийтип содержит все (конечные и бесконечные) списки.Список может быть применен к некоторому значению из множестваиндексов этого списка для определения соответствующего элемента данногосписка.Список характеризуется множеством индексов и эффектом своегоприменения к элементам данного множества индексов.5.7. Типы отображения (Map type expressions)Синтаксис.map_type_expr ::=type_expr ⎯⎯m→ type_exprТерминология. Отображение можно рассматривать как (возможно, пустой)набор пар (v1, v2), где v1 - это некоторое значение из домена отображения, v2 некоторое значение из области значений отображения и v1 отображается в v2.Доменом (областью определения) отображения называется множествозначений v1, для каждого из которых существует некоторое значение v2,такое что пара (v1, v2) входит в данное отображение. Областью значенийотображения является множество значений v2, для каждого из которыхсуществует некоторое значение v1, такое что пара (v1, v2) входит в данноеотображение.Атрибуты.
Максимальным типом выражения map_type_expr видаtype_expr1 ⎯⎯m→ type_expr2 является t1 ⎯⎯m→ t2, где t1 и t2 представляют собоймаксимальные типы выражений type_expr1 и type_expr2 соответственно.Семантика. Типовое выражение map_type_expr представляет тип всехотображений, доменом и областью значений каждого из которых являютсясоответственно некоторое подмножество множества значений типа,представленного первым выражением type_expr, и некоторое подмножествомножества значений, тип которых представлен вторым выражениемtype_expr.Отображение может быть применено к любому значению из его домена сцелью определения соответствующего значения в области значений данногоотображения.Отображение характеризуется доменом и эффектом своего применения кэлементам данного домена.395.8.
Функциональные типы (Function type expressions)Синтаксис.function_type_expr ::=type_expr function_arrow result_descfunction_arrow ::=~ ⏐→→result_desc ::=opt-access_desc-string type_exprТерминология. Выражение для задания функционального типа состоит издвух основных частей: параметрической части (где описывается типпараметра) и результирующей части (где описывается тип результата истатический доступ).
Функция применяется в некотором состоянии кзначению одного какого-либо типа (тип параметра), после чего она может:• вернуть значение другого типа (тип результата);• осуществить доступ к переменным посредством чтения из них илизаписи в них;• осуществить доступ к каналам посредством ввода или вывода по этимканалам.Атрибуты. Максимальным типом выражения function_type_expr вида:~ opt-access_desc-string type_exprtype_expr1 →2или:type_expr1 → opt-access_desc-string type_expr2~ oads t , где t и t представляют собой максимальные типыявляется t1 →212выражений type_expr1 и type_expr2 соответственно и oads задает описаниестатического доступа opt-access_desc-string.Семантика.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
