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

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

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

v : Bool,

f : Int ® Int,

f : Bool ® Nat

axiom

f(v) º 7

В данном случае есть следующие две комбинации интерпретаций для f и v, удовлетворяющие контекстным условиям:

1. f : Int ® Int, v : Int

2. f : Bool ® Nat, v : Bool

Однако для обеих комбинаций максимальный тип выражения f(v) один и тот же (Int) и, следовательно, у данного выражения нет допустимых интерпретаций. Таким образом, данная перегрузка не разрешима.

1. Спецификации (Specifications)

Синтаксис:

specification ::=

module_decl-string

module_decl ::=

scheme_decl │

object_decl

Терминология. Модуль – это либо некоторый объект¹, либо схема.

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

Контекстные условия. Все объявления модулей module_decl должны быть совместимы.

Семантика. Спецификация употребляется для определения одного или более модулей.

1. Объявления (Declarations)

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

Синтаксис:

decl ::=

scheme_decl │

type_decl │

value_decl │

variable_decl │

channel_decl │

axiom_decl

Терминология. Объявление представляет собой список определений (definitions) одинакового вида – схем, типов, значений, переменных, каналов или аксиом. Каждое определение обычно задает некоторый идентификатор или операцию для сущности этого вида, следовательно, обычно оно устанавливает одно или более свойств такой сущности.

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

3.2. Объявление схем (Scheme Declarations)

Синтаксис:

scheme_decl ::=

scheme scheme_def-list

scheme_def ::=

opt-comment-string id opt-formal_scheme_parameter = class_expr

formal_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 является максимальный класс входящего в это определение выражения 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-list

type_def ::=

sort_def │

variant_def │

union_def │

short_record_def │

abbreviation_def

Контекстные условия. Составляющие объявление типов type_decl определения типов type_def должны быть совместимы.

3.3.1. Определение абстрактных типов (Sort Definitions)

Синтаксис:

sort_def ::=

opt-comment-string id

Терминология. Сорт или абстрактный тип – это некоторый тип, не имеющий литералов с предопределенным значением и предопределенных операций за исключением = и  .

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

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

Семантика. Определение sort_def задает конкретный идентификатор id для некоторого абстрактного типа.

Поскольку абстрактный тип не обеспечен предопределенными значениями литералов или операций (кроме = и ) для генерации и манипулирования со своими значениями, составители спецификаций должны сами определять такие значения. Введенные ими определения могут косвенно устанавливать свойства этого абстрактного типа. Если, например, определены два значения одного и того же абстрактного типа и они специфицированы как различные, то косвенно от данного абстрактного типа требуется, чтобы он содержал по крайней мере два значения.

3.3.2. Определение вариантов (Variant Definitions)

Синтаксис:

variant_def ::=

opt-comment-string id == variant-choice

variant ::=

constructor │

record_variant

record_variant ::=

constructor ( component_kind-list )

component_kind ::=

opt-destructor type_expr opt-reconstructor

constructor ::=

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-choice2

name_or_wildcard ::=

type-name │

_

Контекстные условия. Входящие в определение имена name должны представлять типы, причем их максимальные типы должны различаться.

Контекстно-зависимые расширения. Определение union_def вида:

type id = id₁ │ … │ id_n │ _

эквивалентно определению вариантов:

type

id ==

id_from_id₁ ( id_to_id₁ : opt-qualification₁ id₁ ) │ … │

id_from_id_n ( id_to_id_n : opt-qualification_n id_n ) │ _

которое обеспечивает, чтобы все неявное приведение типов в выражениях и образцах (patterns), использующих функции id_from_id_i (1  i  n), было замещено фактическим приведением типов, как будет объяснено в разделах 6.1 и 9.1.

Если определение объединения union_def не содержит универсальной альтернативы ‘_’, соответствующее определение вариантов также не будет содержать такой альтернативы.

3.3.4. Определение сокращенной записи (Short Record Definitions)

Синтаксис:

short_record_def ::=

opt-comment-string id :: component_kind-string

Контекстно-независимые расширения. Определение short_record_def является краткой формой для определения вариантов с единственным вариантом, включающим конструктор. Определение short_record_def вида:

type id :: component_kind₁ … component-kind_n

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

type id == mk_id(component_kind₁, … ,component-kind_n)

где mk_id задает конструктор данного варианта.

3.3.5. Определение абревиатур (Abbreviation Definitions)

Синтаксис:

abbreviation_def ::=

opt-comment-string id = type_expr

Терминология. Определение abbreviation_def является циклическим, если максимальный тип задающего его тип выражения type_expr зависит от типа, который сам задается посредством этого же определения abbreviation_def.

Максимальный тип зависит от некоторого типа t, если он использует этот тип t.

Контекстные условия. Определение abbreviation_def не должно быть циклическим.

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

Максимальное определение для определения abbreviation_def получается путем замещения входящего в него типового выражения type_expr соответствующим выражением для максимального типа.

Семантика. Определение abbreviation_def задает конкретное имя id для типа, представленного выражением type_expr.

3.4. Объявление функций (Value Declarations)

В языке RSL константа рассматривается как частный случай функции, поэтому для объявления констант и функций предусмотрен единый раздел value declarations.

Синтаксис.

value_decl ::=

value value_def-list

value_def ::=

commented_typing │

explicit_value_def │

implicit_value_def │

explicit_function_def │

implicit_function_def │

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

3.4.1. Прокомментированное указание типа (Commented Typing)

См. раздел 8.

3.4.2. Явное определение констант (Explicit Value Definitions)

Синтаксис:

explicit_value_def ::=

opt-comment-string single_typing = pure-value_expr

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

Выражение value_expr должно представлять собой чистое выражение (см. раздел 6.1).

Контекстно-зависимые расширения. Явное определение константы explicit_value_def является краткой формой для определения константы и аксиомы.

Пусть метафункция express преобразует связывание (binding) в выражение путем взятия в скобки всех операций, оставляя остальную часть связывания без изменения. Семантика операций в скобках описана в разделе 10.3. Тогда явное определение константы explicit_value_def вида:

value binding : type_expr = value_expr

является сокращением следующего фрагмента:

value binding : type_expr

axiom express(binding) = value_expr

3.4.3. Неявное определение констант (Implicit Value Definitions)

Синтаксис:

implicit_value_def ::=

opt-comment-string single_typing pure-restriction

Контекстные условия. Ограничение restriction должно представлять собой чистое выражение.

Контекстно-зависимые расширения. Неявное определение константы implicit_value_def является краткой формой для определения константы и аксиомы.

Неявное определение константы implicit_value_def вида:

value binding : type_expr • value_expr

является краткой формой записи следующего фрагмента:

value binding : type_expr

axiom value_expr

3.4.4. Явное определение функций (Explicit Function Definitions)

Синтаксис:

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

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