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

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

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

Максимальным типом 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

Терминология. Декартово произведение – это значение вида (v₁,…,v_n).

Длиной декартова поризведения типов product_type_expr называется количество составляющих его типовых выражений type_expr.

Атрибуты. Максимальным типом выражения product_type_expr вида type_expr₁ ´ … ´ type_expr_n является декартово произведение t₁ ´ … ´ t_n, где t₁, …, t_n являются максимальными типами соответственно выражений type_expr₁, …, type_expr_n.

Семантика. Декартово произведение типов product_type_expr вида type_expr₁ ´ … ´ type_expr_n представляет тип всех декартовых произведений вида (v₁,…,v_n), где тип каждого v_i представлен выражением type_expr_i.

5.5. Множественные типы (Set type expressions)

Синтаксис.

set_type_expr ::=

finite_set_type_expr ½

infinite_set_type_expr

finite_set_type_expr ::=

type_expr-set

infinite_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_expr

finite_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. Если в качестве типового оператора используется ^*, то данный тип содержит все конечные списки. Если типовым оператором является ^w, то соответствующий тип содержит все (конечные и бесконечные) списки.

Список может быть применен к некоторому значению из множества индексов этого списка для определения соответствующего элемента данного списка.

Список характеризуется множеством индексов и эффектом своего применения к элементам данного множества индексов.

5.7. Типы отображения (Map type expressions)

Синтаксис.

map_type_expr ::=

type_expr type_expr

Терминология. Отображение можно рассматривать как (возможно, пустой) набор пар (v₁, v₂), где v₁ - это некоторое значение из домена отображения, v₂ - некоторое значение из области значений отображения и v₁ отображается в v₂. Доменом (областью определения) отображения называется множество значений v₁, для каждого из которых существует некоторое значение v₂, такое что пара (v₁, v₂) входит в данное отображение. Областью значений отображения является множество значений v₂, для каждого из которых существует некоторое значение v₁, такое что пара (v₁, v₂) входит в данное отображение.

Атрибуты. Максимальным типом выражения map_type_expr вида type_expr₁ type_expr₂ является t₁ t₂, где t₁ и t₂ представляют собой максимальные типы выражений type_expr₁ и type_expr₂ соответственно.

Семантика. Типовое выражение map_type_expr представляет тип всех отображений, доменом и областью значений каждого из которых являются соответственно некоторое подмножество множества значений типа, представленного первым выражением type_expr, и некоторое подмножество множества значений, тип которых представлен вторым выражением type_expr.

Отображение может быть применено к любому значению из его домена с целью определения соответствующего значения в области значений данного отображения.

Отображение характеризуется доменом и эффектом своего применения к элементам данного домена.

5.8. Функциональные типы (Function type expressions)

Синтаксис.

function_type_expr ::=

type_expr function_arrow result_desc

function_arrow ::=

½



result_desc ::=

opt-access_desc-string type_expr

Терминология. Выражение для задания функционального типа состоит из двух основных частей: параметрической части (где описывается тип параметра) и результирующей части (где описывается тип результата и статический доступ). Функция применяется в некотором состоянии к значению одного какого-либо типа (тип параметра), после чего она может:

• вернуть значение другого типа (тип результата);

• осуществить доступ к переменным посредством чтения из них или записи в них;

• осуществить доступ к каналам посредством ввода или вывода по этим каналам.

Атрибуты. Максимальным типом выражения function_type_expr вида:

type_expr₁ opt-access_desc-string type_expr₂

или:

type_expr₁  opt-access_desc-string type_expr₂

является t₁ oads t₂, где t₁ и t₂ представляют собой максимальные типы выражений type_expr₁ и type_expr₂ соответственно и oads задает описание статического доступа opt-access_desc-string.

Семантика. Выражение function_type_expr задает тип функций, переводящих тип параметра, представленный выражением type_expr, в тип результата, представленный выражением type_expr конструкции result_desc. Описания доступа access_desc конструкции result_desc специфицируют, к каким переменным и каналам может осуществляться доступ при применении функций. В зависимости от значения метапеременной function_arrow функции являются частично вычислимыми или всюду вычислимыми, как описывается ниже.

• Частично вычислимые (partial) функции

Выражение function_type_expr вида:

type_expr₁ opt-access_desc-string type_expr₂

определяет тип частичных функций из типа, представленного первым выражением type_expr, в тип, представленный вторым выражением type_expr. Этот тип содержит функции, удовлетворяющие следующему ограничению: для любой такой функции f и для любого x, принадлежащего максимальному типу первого выражения type_expr, эффект от применения функционального выражения f(x) в любом состоянии таков, что:

• осуществляется только доступ к переменным и каналам, описанным в конструкции opt-access_desc-string;

• если вычисление выражения завершается (возможно, после выполнения ряда взаимодействий), то результирующее значение принадлежит максимальному типу второго выражения type_expr;

• если вычисление выражения представляет сходящийся процесс (is convergent) и x принадлежит типу, представленному первым выражением type_expr, то результирующее значение принадлежит типу, представленному вторым выражением type_expr.

 Всюду вычислимые (total) функции

Выражение function_type_expr вида:

type_expr  result_desc

представляет собой краткую запись выражения:

{½ f : type_expr result_desc •  x : type_expr • f(x) post true ½}

которое обеспечивает, что f и x не являются свободными переменными выражений type_expr и result_desc.

Это означает, что выражение function_type_expr вида:

type_expr₁  opt-access_desc-string type_expr₂

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

type_expr₁ opt-access_desc-string type_expr₂

которые удовлетворяют следующему ограничению: для любой такой функции f и для любого x, принадлежащего типу, представленному первым выражением type_expr, эффект от применения функционального выражения f(x) в любом состоянии представляет собой сходящийся процесс.

5.9. Подтипы (Subtype Expressions)

Синтаксис.

subtype_expr ::=

{ single_typing pure-restriction }

Контекст и правила видимости. Контекстом указания типа 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.

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

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