rsl.formal.specifications.conspect (811084), страница 6
Текст из файла (страница 6)
Определение канала single_channel_def задает конкретныйидентификатор id для некоторого канала, по которому могут передаватьсязначения, тип которых представлен выражением type_expr.3.7. Объявление аксиом (Axiom Declarations)Синтаксис:axiom_decl ::=axiom opt-axiom_quantification axiom_def-listaxiom_quantification ::=forall typing-list •axiom_def ::=opt-comment-string opt-axiom_naming readonly_logical-value_expraxiom_naming ::=[ id ]Контекстно-независимые расширения. Любое объявлениеaxiom_decl может быть расширено до объявления следующего вида:аксиомaxiomopt-axiom_naming1 □ value_expr1,•••opt-axiom_namingn □ value_exprnВ случае отсутствия конструкции axiom_quantification объявление аксиомaxiom_decl вида:axiomopt-axiom_naming1 value_expr1,•••opt-axiom_namingn value_exprn30является краткой формой объявления:axiomopt-axiom_naming1 □ value_expr1,•••opt-axiom_namingn □ value_exprnКонструкция axiom_quantification является сокращенной записьюдистрибутивной квантификации, т.е.
объявление axiom_decl вида:дляaxiom forall typing-list •opt-axiom_naming1 value_expr1,•••opt-axiom_namingn value_exprnпредставляет собой краткую форму записи объявления:axiomopt-axiom_naming1 □ ∀ typing-list • value_expr1,•••opt-axiom_namingn □ ∀ typing-list • value_exprnКонтекстные условия. Все входящие в объявление аксиом axiom_declопределения axiom_def должны быть совместимы.Входящее в определение аксиомы axiom_def выражение value_expr должнобыть доступно только для чтения (read-only), и его максимальный типдолжен быть Bool.Семантика.
Определение axiom_def устанавливает в терминах некоторойаксиомы (в виде соответствующего булевского выражения value_expr)свойства сущностей, заданных где-то в другом месте спецификации.Аксиома может быть снабжена именем (id в конструкции axiom_naming).4. Описание классов (Class Expressions)4.1.
Общие положенияСинтаксис:class_expr ::=basic_class_expr │extending_class_expr │hiding_class_expr │renaming_class_expr │scheme_instantiationТерминология. Модель представляет собой некоторую ассоциациюидентификаторов и операций с какими-либо сущностями. Модельобеспечивает какой-либо идентификатор или операцию, если онаассоциирует этот идентификатор или операцию с некоторой сущностью.Модель удовлетворяет определению, если она обеспечивает идентификаторили операцию, заданные этим определением, если сущность, ассоциируемая31с данным идентификатором или операцией, является сущностьюопределяемого вида и, наконец, если свойства, устанавливаемые указаннымопределением, сохраняются в данной модели.Класс представляет собой набор моделей.Идентификаторилиоперацияявляетсянедоспецифицированным(under-specified), если в классе существует по крайней мере две модели, вкоторых данный идентификатор или операция ассоциируется с различнымисущностями.Класс class_expr1 является подклассом класса class_expr2, если все моделикласса class_expr1 являются моделями класса class_expr2.Для задания классов используются классовые выражения (class expressions).Некоторые классы называются максимальными.
Классовое выражениепредставляет максимальный класс тогда и только тогда, когда всеопределения, заданные этим выражением, являются максимальными.Определение схемы является максимальным, если его классовое выражениеявляется максимальным.Определение типа является максимальным, если заданный с помощью этогоопределения идентификатор типа представляет максимальный тип.Определение функции (value definition) является максимальным, еслипредставляет собой указание типа, в котором типовое выражение являетсямаксимальным.Определение переменной является максимальным, если представляет собойопределение одной отдельной переменной без инициализации, типовоевыражение которой является максимальным.Определение канала является максимальным, если представляет собойопределение одного отдельного канала, типовое выражение которогоявляется максимальным.Определение аксиомы не является максимальным.Атрибуты.
С каждым выражением для задания класса ассоциируетсянекоторый максимальный класс. Конкретный максимальный класс длякаждого вида классовых выражений определяется в соответствующемразделе данного пособия.Класс, представленный некоторым классовым выражением, являетсяподклассом ассоциируемого с данным выражением максимального класса.Семантика. Классовое выражение class_expr употребляется для обозначениянабора определений и представляет класс, состоящий из всех моделей,которые удовлетворяют каждому из этих определений. Каждая модельассоциирует идентификаторы и операции, определенные в классовомвыражении class_expr, с конкретными сущностями.
Для каждойразновидности классового выражения в соответствующем разделе пособиябудет указано, какие именно определения задает это выражение class_expr.324.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_itemdisambiguated_item ::=id_or_op : type_expr33Контекстные условия. В конструкции disambiguated_item метапеременнаяid_or_op должна представлять некоторую функцию, причем ее максимальныйтип должен совпадать с максимальным типом выражения type_expr.Семантика. Типовое выражение type_exprвнутри конструкцииdisambiguated_item требуется в тех случаях, когда id_or_op за счет перегрузкиимен (overloading) представляет несколько значений с различнымимаксимальными типами.
В таких случаях выражение type_exprидентифицирует в точности одно из этих значений.5. Описание типов (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 recorddefinitions, см. раздел 3.3.4.).• составные типы построены из других типов путем применениятипового оператора (type operator) к одному или более типов.Будем говорить, что тип является чистым функциональным типом, если онможет быть представлен некоторым выражением функционального типа, вкотором отсутствует строка описания доступа.Тип t1 является подтипом типа t2, если все значения, принадлежащие типу t1,принадлежат также типу t2 .Некоторые типы называются максимальными. Тип является максимальным,если он может быть представлен максимальным типовым выражением.34Типовое выражение является максимальным тогда и только тогда, когда оноявляется одним из следующих:• Unit, Bool, Int, Real или Char (т.е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
