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

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

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

Для задания классов используются классовые выражения (class expressions).

Некоторые классы называются максимальными. Классовое выражение представляет максимальный класс тогда и только тогда, когда все определения, заданные этим выражением, являются максимальными.

Определение схемы является максимальным, если его классовое выражение является максимальным.

Определение типа является максимальным, если заданный с помощью этого определения идентификатор типа представляет максимальный тип.

Определение функции (value definition) является максимальным, если представляет собой указание типа, в котором типовое выражение является максимальным.

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

Определение канала является максимальным, если представляет собой определение одного отдельного канала, типовое выражение которого является максимальным.

Определение аксиомы не является максимальным.

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

Класс, представленный некоторым классовым выражением, является подклассом ассоциируемого с данным выражением максимального класса.

Семантика. Классовое выражение class_expr употребляется для обозначения набора определений и представляет класс, состоящий из всех моделей, которые удовлетворяют каждому из этих определений. Каждая модель ассоциирует идентификаторы и операции, определенные в классовом выражении class_expr, с конкретными сущностями. Для каждой разновидности классового выражения в соответствующем разделе пособия будет указано, какие именно определения задает это выражение class_expr.

4.2. Базисные классы (Basic Class Expressions)

Синтаксис:

basic_class_expr ::=

class opt-decl-string end

Контекст и правила видимости. Непосредственным контекстом конструкции opt-decl-string является сама opt-decl-string. Это означает, что порядок следования определений в конструкции opt-decl-string несущественен.

Контекстные условия. Все входящие в данное выражение объявления decl должны быть совместимы.

Атрибуты. Максимальный класс выражения basic_class_expr задается выражением class_expr, состоящим из максимальных определений, полученных из не аксиоматических определений, входящих в состав объявлений указанного выражения basic_class_expr.

Значение. Выражение basic_class_expr употребляется для обозначения определений, появляющихся в объявлениях decls.

4.3. Расширяющие классы (Extending Class Expressions)

Синтаксис:

extending_class_expr ::=

extend class_expr with class_expr

Контекст и правила видимости. Контекст первого классового выражения class_expr расширяется до второго классового выражения class_expr.

Контекстные условия. Выражения class_expr должны быть совместимы.

Атрибуты. Максимальный класс представляется выражением, формируемым из исходного выражения extending_class_expr, путем замены входящих в него выражений class_expr максимальными.

Семантика. Классовое выражение extending_class_expr используется для обозначения тех определений, которые обозначаются выражениями class_expr.

4.4. Определяемые операции (Defined Items)

Синтаксис:

defined_item ::=

id_or_op │

disambiguated_item

disambiguated_item ::=

id_or_op : type_expr

Контекстные условия. В конструкции disambiguated_item метапеременная id_or_op должна представлять некоторую функцию, причем ее максимальный тип должен совпадать с максимальным типом выражения type_expr.

Семантика. Типовое выражение type_expr внутри конструкции disambiguated_item требуется в тех случаях, когда id_or_op за счет перегрузки имен (overloading) представляет несколько значений с различными максимальными типами. В таких случаях выражение type_expr идентифицирует в точности одно из этих значений.

1. Описание типов (Type Expressions)

5.1. Общие положения

Синтаксис:

type_expr ::=

type_literal │

type-name │

product_type_expr │

set_type_expr │

list_type_expr │

map_type_expr │

function_type_expr │

subtype_type_expr │

bracketed_type_expr

Терминология. Тип представляет собой набор значений. Различаются три вида типов:

• предопределенные типы представлены встроенными в язык литералами. Такие типы включают, например, целые числа или булевские значения. Подробнее см. раздел 5.2.

• абстрактные типы представлены идентификаторами, которые вводятся в определениях абстрактных типов (sort definitions, см. раздел 3.3.1.), вариантов (variant definitions, см. раздел 3.3.2.), объединений (union definitions, см. раздел 3.3.3.) и сокращенных записей (short record definitions, см. раздел 3.3.4.).

• составные типы построены из других типов путем применения типового оператора (type operator) к одному или более типов.

Будем говорить, что тип является чистым функциональным типом, если он может быть представлен некоторым выражением функционального типа, в котором отсутствует строка описания доступа.

Тип t₁ является подтипом типа t₂, если все значения, принадлежащие типу t₁, принадлежат также типу t₂ .

Некоторые типы называются максимальными. Тип является максимальным, если он может быть представлен максимальным типовым выражением.

Типовое выражение является максимальным тогда и только тогда, когда оно является одним из следующих:

• Unit, Bool, Int, Real или Char (т.е. любым типом, состоящим из литералов, за исключением Nat и Text).

• именем, соответствующее определение которого представляет собой определение абстрактного типа, варианта, объединения или сокращенной записи.

• именем, соответствующее определение которого является определением аббревиатуры, в состав которого входит максимальное типовое выражение.

• типовым выражением, построенным из максимальных типовых выражений и описаний статического доступа путем применения одного из типовых операторов  , -infset, ^ω, или (т.е. любых типовых операторов за исключением -set, ^* и ).

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

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

Два максимальных типа считаются неразличимыми тогда и только тогда, когда существуют два типовых выражения, представляющие эти типы и различающиеся не больше, чем описаниями статического доступа содержащихся в них функциональных типов.

Два максимальных типа считаются различимыми тогда и только тогда, когда они не являются неразличимыми.

Использование в спецификации определений объединений (union definitions) вызывает потенциальное приведение типов, которое является частичной функцией между максимальными типами.

Будем говорить, что имеет место потенциальное приведение (potential coercion) максимального типа t₁ к максимальному типу t₂ тогда и только тогда, когда выполняются следующие условия:

1. t₁ идентичен с t₂, в этом случае потенциальное приведение типа t₁ к t₂ представляет собой тождественную функцию.

2. задано определение объединения вида:

id₂ = …  id₁  …

в котором id₁ имеет максимальный тип t₁ и id₂ имеет максимальный тип t₂, в этом случае потенциальное приведение типа t₁ к типу t₂ представляет собой функцию id₂_from_id₁.

1. заданы типы t₁₁, t₁₂, t₂₁, t₂₂ и описание статического доступа opt‑access_desc-string такие, что имеется потенциальное приведение типов t₁₁ к t₂₁ и t₁₂ к t₂₂, кроме того, типы t₁ и t₂ построены одним из перечисленных ниже способов. В этом случае потенциальное приведение типа t₁ к типу t₂ выводится из других потенциальных приведений очевидным образом.

1. t₁ есть …´ t₁₁  … и t₂ есть … ´ t₂₁ ´ …

2. t₁ есть t₁₁–infset и t₂ есть t₂₁-infset.

3. t₁ есть t₁₁^ и t₂ есть t₂₁^.

4. t₁ есть t₁₁ t₁₂ и t₂ есть t₂₁ t₂₂.

5. t₁ есть t₁₁ opt-access_desc-string t₁₂ и

t₂ есть t₂₁ opt-access_desc-string t₂₂.

4. задан тип t₃ такой, что f₁₃ является потенциальным приведением типа t₁ к t₃ и f₃₂ соответствующим приведением t₃ к t₂; в этом случае потенциальным приведением типа t₁ к t₂ является f₃₂  f₁₃.

Максимальный тип t₁ называется приводимым к максимальному типу t₂, если существует одно и только одно потенциальное приведение типа t₁ к t₂.

Максимальный тип t₁ меньше или равен максимального типа t₂, если он приводим к подтипу типа t₂.

Максимальный тип t называется верхней границей набора максимальных типов, если все максимальные типы данного набора меньше или равны t.

Максимальный тип называется наименьшей верхней границей набора максимальных типов, если он является верхней границей данного набора и меньше или равен всех остальных верхних границ этого набора.

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

Семантика. Типовое выражение type_expr представляет некоторый тип. Конкретные типы для каждой разновидности типовых выражений определяются в следующих разделах.

5.2. Предопределенные типы (Type Literals)

Синтаксис.

type_literal ::=

Unit 

Bool 

Int 

Nat 

Real 

Text 

Char

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

Максимальным типом Bool является Bool.

Максимальным типом Int является Int.

Максимальным типом Nat является Int.

Максимальным типом Real является Real.

Максимальным типом Text является Char^.

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

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