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

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

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

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

Семантика. Секция содержит описание семантики статически корректных строк языка.

1.2. Декларативные конструкции

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

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

С любым определением связана некоторая область RSL текста, называемая контекстом этого определения. Внутри этого контекста и только там для обращения к вводимой данным определением сущности можно использовать ее идентификатор или операцию. Под контекстом декларативной конструкции подразумевается контекст ее определений, который устанавливается правилами контекста языка RSL.

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

Два определения называются совместимыми (compatible), если они задают различные идентификаторы (операции) или если оба они являются определениями значений (констант и функций), которые задают один и тот же идентификатор (операцию), но их максимальные типы различимы.

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

1.3. Правила контекста (Scope Rules)

Контекст декларативной конструкции может зависеть от контекста, в котором она встречается. Поэтому для каждой конструкции, включающей в себя декларативную конструкцию, должен быть задан контекст такого включения. Это описывается в секциях “Контекст и правила видимости” с использованием следующих соглашений:

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

local

value x : Int = 3

in x + 2 end

Контекстом определения x является строка локального объявления и выражение x + 2.

1. Для декларативной конструкции, встречающейся непосредственно внутри декларативной конструкции, возможны следующие случаи:

1. Контекст указан явно. В этом случае итоговый контекст совпадает с этим явно указанным контекстом.

2. Указан непосредственный контекст. В этом случае итоговым контекстом является непосредственный контекст плюс возможные расширения. Расширения зависят от контекста внешней декларативной конструкции и задаются для всех ее вхождений.

Например, объявления в базисном классовом выражении:

scheme S =

extend

class

value x : Int = 3,

end

with

class

value y : Int = x

end

Непосредственным контекстом определения x является строка объявлений первого классового выражения. Итоговым контекстом x является эта область плюс строка объявлений второго классового выражения.

1. Контекст не задан. В этом случае неявно подразумевается, что контекст внутренней конструкции задается контекстом непосредственно объемлющей ее внешней конструкции. Например:

value

x : Int = y,

y : Int

Контекст определения значения x равен контексту всего раздела объявления значений.

1.4. Правила видимости (Visibility Rules)

Правила видимости языка RSL таковы:

1. Определение не видимо вне своего контекста.

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

Например:

class

variable v : Bool := true

axiom

local

variable v : Int := 3

in v = 7 end

end

В этом примере контекстом определения переменной v : Bool := true является все классовое выражение, тогда как контекстом определения локальной переменной v : Int := 3 является только строка локального объявления и выражение v = 7. Следовательно, по правилу 2 в выражении v = 7 видимым является только определение локальной переменной. Действительно, внутреннее определение v будет всегда скрывать внешнее внутри своего

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

class

value v : Bool = true

axiom

local

value v : Int = 3

in v end

end

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

1.5. Перегрузка имен (Overloading)

Под перегрузкой идентификатора или операции в некоторой точке RSL текста понимается ситуация, когда в указанной точке видимыми являются несколько определений этого идентификатора или операции.

Перегрузка имен допускается только для операций и идентификаторов значений (констант и функций).

У всех операций есть одно или более предопределенное значение, контекстом которого является вся спецификация целиком и которое не может скрываться. Следовательно, если пользователь определяет некоторую операцию таким образом, что ее максимальный тип различается с максимальными типами ее предопределенных значений, то эта операция перегружается в тех точках, где видимыми являются как определение пользователя, так и предопределенные значения указанной операции. Пользователю не разрешается определять операцию так, чтобы ее максимальный тип не различался хотя бы с одним из максимальных типов ее предопределенных значений (см. контекстные условия в разделе 11).

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

Некоторые возможные интерпретации рассматриваемого идентификатора или операции могут оказаться недопустимыми, поскольку не будут удовлетворять контекстным условиям его вхождения. Поэтому, чем больше контекста будет принято во внимание, тем больше информации (контекстных условий) будет получено для исключения недопустимых интерпретаций. Однако если рассматриваемый контекст представляет собой выражение, максимальный тип которого будет одним и тем же для нескольких возможных интерпретаций входящих в него идентификаторов или операций, то дальнейший анализ контекста не даст ощутимых результатов, т.к. не позволит отдать предпочтение какой-то одной из имеющихся интерпретаций. Следовательно, все эти интерпретации будут допустимыми.

Более формально для данной конструкции допустимые интерпретации (legal interpretation) вхождений идентификаторов или операций в точке их использования находятся следующим образом:

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

2. Далее удаляются те комбинации, которые не удовлетворяют контекстным условиям данной конструкции.

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

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

Перегрузка называется разрешимой (resolvable), если существует в точности одна допустимая интерпретация каждого идентификатора и операции в его ближайшем объемлющем ‘разрешающем контексте’. При этом под разрешающим контекстом понимается одна из следующих ситуаций:

• выражение value_expr в ограничении списка list_limitation;

• выражение value_expr в let-выражении explicit_let;

• выражение value_expr в case-выражении case_expr;

• выражение value_expr в пост-выражении post_expr;

• определяемая операция defined_item, представляющая собой конструкцию id_or_op;

• спецификация specification.

Рассмотрим несколько примеров, иллюстрирующих ситуацию перегрузки идентификаторов и операций.

Пример 1:

class

value

v : Int,

v : Bool

axiom

v

end

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

Пример 2:

class

value

+ : Bool  Bool  Bool,

v : Real

axiom

true + false  true,

v  1.7 + 2.2

end

Здесь перегружаются два вхождения операции + в аксиомы, и каждое вхождение имеет три возможные интерпретации: предопределенное целочисленное сложение (с максимальным типом Int ´ Int Int), или предопределенное вещественное сложение (с максимальным типом Real ´ Real Real), или определенное пользователем булевское сложение (с максимальным типом Bool ´ Bool Bool). Для первого вхождения операции + контекстным условиям удовлетворяет только определенное пользователем сложение, а для второго вхождения — только предопределенное вещественное сложение. Таким образом, для каждого из двух указанных вхождений операции +, есть в точности одна его допустимая интерпретация и, следовательно, данная перегрузка разрешима.

Пример 3:

value

v : Int,

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

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