rsl.formal.specifications.conspect (811084), страница 3
Текст из файла (страница 3)
При этом подразрешающим контекстом понимается одна из следующих ситуаций:• выражение value_expr в ограничении списка list_limitation;• выражение value_expr в let-выражении explicit_let;• выражение value_expr в case-выражении case_expr;• выражение value_expr в пост-выражении post_expr;defined_item,представляющаясобой• определяемаяоперацияконструкцию id_or_op;• спецификация specification.Рассмотрим несколько примеров, иллюстрирующих ситуацию перегрузкиидентификаторов и операций.13Пример 1:classvaluev : Int,v : BoolaxiomvendВ данном случае имеет место перегрузка вхождения v в аксиому, т.к. у негоесть две возможные интерпретации: либо это целочисленное значение, либобулевское.
Однако только последняя интерпретация удовлетворяетконтекстным условиям (максимальным типом аксиомы должен быть типBool) и, следовательно, только эта интерпретация допустима. Таким образом,данная перегрузка является разрешимой, поскольку существуетединственная допустимая интерпретация вхождения v.Пример 2:classvalue+ : Bool × Bool → Bool,v : Realaxiomtrue + false ≡ true,v ≡ 1.7 + 2.2endЗдесь перегружаются два вхождения операции + в аксиомы, и каждоевхождение имеет три возможные интерпретации: предопределенное~ Int), илицелочисленное сложение (с максимальным типом Int × Int →предопределенное вещественное сложение (с максимальным типом~ Real), или определенное пользователем булевское сложение (сReal × Real →~ Bool).
Для первого вхождения операциимаксимальным типом Bool × Bool →+ контекстным условиям удовлетворяет только определенное пользователемсложение, а для второго вхождения — только предопределенноевещественное сложение. Таким образом, для каждого из двух указанныхвхождений операции +, есть в точности одна его допустимая интерпретацияи, следовательно, данная перегрузка разрешима.Пример 3:valuev : Int,v : Bool,f : Int → Int,f : Bool → Nataxiomf(v) ≡ 714В данном случае есть следующие две комбинации интерпретаций для f и v,удовлетворяющие контекстным условиям:1. f : Int → Int, v : Int2.
f : Bool → Nat, v : BoolОднако для обеих комбинаций максимальный тип выражения f(v) один и тотже (Int) и, следовательно, у данного выражения нет допустимыхинтерпретаций. Таким образом, данная перегрузка не разрешима.2. Спецификации (Specifications)Синтаксис:specification ::=module_decl-stringmodule_decl ::=scheme_decl │object_declТерминология. Модуль – это либо некоторый объект1, либо схема.Контекст и правила видимости.
Контекстом входящих в спецификациюобъявлений module_decl-string являются сами эти объявления module_declstring. Это означает, что порядок следования определений не существенен,т.е. схема может быть использована до своего определения.Контекстные условия. Все объявления модулей module_decl должны бытьсовместимы.Семантика. Спецификация употребляется для определения одного илиболее модулей.3. Объявления (Declarations)3.1. Общие положенияСинтаксис:decl ::=scheme_decl │type_decl │value_decl │variable_decl │channel_decl │axiom_declТерминология. Объявление представляет собой список определений(definitions) одинакового вида – схем, типов, значений, переменных, каналовили аксиом.
Каждое определение обычно задает некоторый идентификатор1Как уже отмечалось, далее объекты RSL рассматриваться не будут.15или операцию для сущности этого вида, следовательно, обычно оноустанавливает одно или более свойств такой сущности.Атрибуты. За исключением определений аксиом с каждым видомопределенийсвязанонекотороемаксимальноеопределение.Всоответствующих разделах для каждого вида определений описываетсямаксимальное определение, специфичное для данного вида.3.2. Объявление схем (Scheme Declarations)Синтаксис:scheme_decl ::=scheme scheme_def-listscheme_def ::=opt-comment-string id opt-formal_scheme_parameter = class_exprformal_scheme_parameter ::=( formal_scheme_argument-list )formal_scheme_argument ::=object_defТерминология. Схема представляет собой класс или параметризованныйкласс.
Параметризованный класс – это отображение списка объектов наклассы: каждый объект списка отображается в некоторый класс.Максимальнымклассомсхемыявляетсямаксимальныйкласссоответствующего выражения, задающего класс в определении даннойсхемы.Определение схемы scheme_def является циклическим, если конструкцииopt-formal_array_parameter или class_expr зависят от схемы, которая самазадается этим определением scheme_def.Конструкция зависит от схемы S, если она, игнорируя ограничения ввыражениях для подтипов, использует S или любую схему, содержащуюопределение, в котором opt-formal_scheme_parameter или class_expr зависят отS.Контекст и правила видимости. В определении схемы scheme_defконтекстом необязательного параметра opt-formal_scheme_parameter являетсясам этот параметр opt-formal_scheme_parameter и выражение class_expr,входящее в данное определение схемы.Контекстные условия.
Все входящие в объявление схемы scheme_declопределения scheme_def должны быть совместимы.Входящие в формальный параметр схемы formal_scheme_parameter аргументыformal_scheme_argument должны быть совместимы.Определение схемы scheme_def не должно быть циклическим.Атрибуты. В определении схемы scheme_def максимальным классомидентификатора id является максимальный класс входящего в это16определение выражения class_expr, и в случае присутствия необязательногопараметра formal_scheme_parameter идентификатор id имеет такжеформальный параметр, которым и является formal_scheme_parameter.Максимальное определение определения схемы scheme_def получается изисходного определения путем замещения в его составе определенийобъектов, входящих в formal_scheme_parameter (в случае его присутствия), насоответствующие максимальные определения этих объектов и выраженияclass_expr на соответствующее выражение для максимального класса.Семантика.
Определение схемы scheme_def задает конкретныйидентификатор id для определяемой схемы.• Определение схемы в форме:id = class_exprзадает конкретный идентификатор id для класса, представленноговыражением class_expr.• Определение схемы в виде:id(formal_scheme_argument-list) = class_exprзадает идентификатор id для параметризованного класса.3.3. Объявление типов (Type Declarations)Синтаксис:type_decl ::=type type_def-listtype_def ::=sort_def │variant_def │union_def │short_record_def │abbreviation_defКонтекстные условия.
Составляющие объявлениеопределения типов type_def должны быть совместимы.типовtype_decl3.3.1. Определение абстрактных типов (Sort Definitions)Синтаксис:sort_def ::=opt-comment-string idТерминология. Сорт или абстрактный тип – это некоторый тип, неимеющий литералов с предопределенным значением и предопределенныхопераций за исключением = и ≠ .17Атрибуты. Максимальным типом входящего в определение идентификатораid является тип, представленный этим идентификатором id.Определение абстрактного типа является максимальным.Семантика. Определение sort_def задает конкретный идентификатор id длянекоторого абстрактного типа.Поскольку абстрактный тип не обеспечен предопределенными значениямилитералов или операций (кроме = и ≠) для генерации и манипулирования сосвоими значениями, составители спецификаций должны сами определятьтакие значения. Введенные ими определения могут косвенно устанавливатьсвойства этого абстрактного типа.
Если, например, определены два значенияодного и того же абстрактного типа и они специфицированы как различные,то косвенно от данного абстрактного типа требуется, чтобы он содержал покрайней мере два значения.3.3.2. Определение вариантов (Variant Definitions)Синтаксис:variant_def ::=opt-comment-string id == variant-choicevariant ::=constructor │record_variantrecord_variant ::=constructor ( component_kind-list )component_kind ::=opt-destructor type_expr opt-reconstructorconstructor ::=id_or_op │_destructor ::=id_or_op :reconstructor ::=↔ id_or_opКонтекстно-независимые расширения. Определение варианта variant_defявляется сокращением (краткой формой) для определения абстрактного типа,его конструкторов, деструкторов и реконструкторов.3.3.3.
Определение объединений (Union Definitions)Синтаксис:union_def ::=opt-comment-string id = name_or_wildcard-choice218name_or_wildcard ::=type-name │_Контекстные условия. Входящие в определение имена name должныпредставлять типы, причем их максимальные типы должны различаться.Контекстно-зависимые расширения. Определение union_def вида:type id = id1 │ … │ idn │ _эквивалентно определению вариантов:typeid ==id_from_id1 ( id_to_id1 : opt-qualification1 id1 ) │ … │id_from_idn ( id_to_idn : opt-qualificationn idn ) │ _которое обеспечивает, чтобы все неявное приведение типов в выражениях иобразцах (patterns), использующих функции id_from_idi (1 ≤ i ≤ n), былозамещено фактическим приведением типов, как будет объяснено в разделах6.1 и 9.1.Если определение объединения union_def не содержит универсальнойальтернативы ‘_’, соответствующее определение вариантов также не будетсодержать такой альтернативы.3.3.4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
