rsl.formal.specifications.conspect (811084), страница 2
Текст из файла (страница 2)
Секция содержит расширенияопределяемых конструкций. При задании контекстно-независимогорасширения какой-либо конструкции в терминах других конструкций ееконтекст, правила видимости, контекстные условия, атрибуты и семантикане формулируются отдельно, а задаются соответственно контекстом,правилами видимости и т.д.
ее расширения.Неявно предполагается, что все конструкции, содержащие комментарии(принадлежащие к синтаксической категории comment), имеют контекстнонезависимое расширение до соответствующей конструкции, получаемойпутем удаления этих комментариев.Контекст (scope) и правила видимости. Секция содержит описаниеконтекста и правил видимости.Контекстные условия. Секция содержит описание условий, которымдолжны удовлетворять синтаксически правильные строки для обеспечения8их статической корректности. При этом статически корректной называетсясинтаксически правильная строка, для которой выполнены контекстныеусловия. Для удобства некоторые из этих условий в синтаксическихправилах также изображаются с помощью напечатанных курсивомпрефиксов, как описано выше.Контекстно-зависимые расширения.
Секция содержит расширениеконструкций. Когда для какой-либо конструкции задается контекстнозависимое расширение в терминах других конструкций, ее атрибуты исемантика не формулируются отдельно, а задаются атрибутами и семантикойее расширения. Контекстные условия расширяемой конструкциипредставляют собой контекстные условия, сформулированные для даннойконструкции, плюс контекстные условия ее расширения.Атрибуты. Секция содержит описание атрибутов для статическикорректных строк. Атрибуты используются для описания контекстныхусловий.Семантика. Секция содержит описание семантики статически корректныхстрок языка.1.2. Декларативные конструкцииДекларативнаяконструкцияявляетсяязыковойконструкцией,представляющей одно или более определений.
Определение задаетидентификатор или операцию для некоторой сущности, такой как схема, тип,значение, переменная, канал или аксиома.Для некоторых декларативных конструкций определения, которые онипредставляют, зависят от контекста, в котором встречаются эти конструкции.Для таких конструкций максимальные типы идентификаторов и (или)операций, заданных содержащимися в данных конструкциях определениями,определяются максимальным типом, заданным контекстом этихконструкций. Такой максимальный тип называют максимальнымконтекстным типом данной декларативной конструкции.С любым определением связана некоторая область RSL текста, называемаяконтекстом этого определения. Внутри этого контекста и только там дляобращения к вводимой данным определением сущности можно использоватьее идентификатор или операцию.
Под контекстом декларативнойконструкции подразумевается контекст ее определений, которыйустанавливается правилами контекста языка RSL.Определение является видимым в некоторой точке RSL текста, если в даннойточке для обращения к заданной с помощью этого определения сущностиможно использовать ее идентификатор или операцию. В таком случаеговорят, что в данной точке идентификатор или операция представляютданную сущность или являются ее именем. Видимость определенийустанавливается правилами видимости языка RSL.9Два определения называются совместимыми (compatible), если они задаютразличные идентификаторы (операции) или если оба они являютсяопределениями значений (констант и функций), которые задают один и тотже идентификатор (операцию), но их максимальные типы различимы.Контекстные условия, установленные для каждой индивидуальнойсинтаксической категории, обеспечивают совместимость всех видимыхопределений в любой точке RSL текста.1.3. Правила контекста (Scope Rules)Контекст декларативной конструкции может зависеть от контекста, вкотором она встречается.
Поэтому для каждой конструкции, включающей всебя декларативную конструкцию, должен быть задан контекст такоговключения. Это описывается в секциях “Контекст и правила видимости” сиспользованием следующих соглашений:1. Для декларативной конструкции, встречающейся непосредственновнутри не декларативной конструкции, контекст всегда указываетсяявно. Например, объявления в локальном выражении:localvalue x : Int = 3in x + 2 endКонтекстом определения x является строка локального объявления ивыражение x + 2.2. Для декларативной конструкции, встречающейся непосредственновнутри декларативной конструкции, возможны следующие случаи:(a) Контекст указан явно.
В этом случае итоговый контекст совпадаетс этим явно указанным контекстом.(b) Указан непосредственный контекст. В этом случае итоговымконтекстом является непосредственный контекст плюс возможныерасширения. Расширения зависят от контекста внешнейдекларативной конструкции и задаются для всех ее вхождений.Например, объявления в базисном классовом выражении:scheme S =extendclassvalue x : Int = 3,endwithclassvalue y : Int = xendНепосредственным контекстом определения x является строкаобъявлений первого классового выражения. Итоговым контекстом10x является эта область плюс строка объявлений второго классовоговыражения.(c) Контекст не задан. В этом случае неявно подразумевается, чтоконтекствнутреннейконструкциизадаетсяконтекстомнепосредственно объемлющей ее внешней конструкции.Например:valuex : Int = y,y : IntКонтекст определения значения x равен контексту всего разделаобъявления значений.1.4.
Правила видимости (Visibility Rules)Правила видимости языка RSL таковы:1. Определение не видимо вне своего контекста.2. Определение потенциально видимо всюду внутри своего контекста.Однако в этом контексте могут существовать участки, где определениеявляется скрытым, т.е. не видимым. Например, если идентификатор(операция), заданный некоторым определением, задается также вовнутреннем контексте с помощью другого определения, то внешнееопределение считается скрытым на протяжении всего контекста этоговнутреннего определения.
В случае, когда оба такие определенияпредставляют собой определения значений, внешнее определение нескрывается, если максимальные типы этих двух значений различимы.Например:classvariable v : Bool := trueaxiomlocalvariable v : Int := 3in v = 7 endendВ этом примере контекстом определения переменной v : Bool := true являетсявсе классовое выражение, тогда как контекстом определения локальнойпеременной v : Int := 3 является только строка локального объявления ивыражение v = 7. Следовательно, по правилу 2 в выражении v = 7 видимымявляется только определение локальной переменной.
Действительно,внутреннее определение v будет всегда скрывать внешнее внутри своего11контекста, если только оба они не являются определениями значений. Этоиллюстрирует следующий пример:classvalue v : Bool = trueaxiomlocalvalue v : Int = 3in v endendЗдесь в локальном выражении определение локального значения не скрываетвнешнее определение значения, поскольку максимальные типы этих двухопределений различны.
В данном локальном выражении видимыми будутоба определения значения, фактически же вхождение v должно определятьсявнешним определением, т.к. аксиомы представляют собой булевскиевыражения.1.5. Перегрузка имен (Overloading)Под перегрузкой идентификатора или операции в некоторой точке RSLтекста понимается ситуация, когда в указанной точке видимыми являютсянесколько определений этого идентификатора или операции.Перегрузка имен допускается только для операций и идентификаторовзначений (констант и функций).У всех операций есть одно или более предопределенное значение,контекстом которого является вся спецификация целиком и которое неможет скрываться.
Следовательно, если пользователь определяет некоторуюоперацию таким образом, что ее максимальный тип различается смаксимальными типами ее предопределенных значений, то эта операцияперегружается в тех точках, где видимыми являются как определениепользователя, так и предопределенные значения указанной операции.Пользователю не разрешается определять операцию так, чтобы еемаксимальный тип не различался хотя бы с одним из максимальных типов еепредопределенных значений (см. контекстные условия в разделе 11).При составлении спецификаций необходимо иметь в виду, что для тогочтобы спецификация оказалась полезной и могла быть использована вдальнейшем, у каждого ее идентификатора и операции должна существоватьединственная допустимая интерпретация.
При этом под интерпретациейидентификатора (операции) понимается его соответствующее определение.При перегрузке какого-то идентификатора или операции его вхождениеимеет несколько возможных интерпретаций (по одной для каждого еговидимого определения), и, следовательно, возникает проблема найтидопустимое соответствующее определение данного идентификатора илиоперации (если оно вообще существует).12Некоторые возможные интерпретации рассматриваемого идентификатораили операции могут оказаться недопустимыми, поскольку не будутудовлетворять контекстным условиям его вхождения. Поэтому, чем большеконтекста будет принято во внимание, тем больше информации(контекстных условий) будет получено для исключения недопустимыхинтерпретаций. Однако если рассматриваемый контекст представляет собойвыражение, максимальный тип которого будет одним и тем же длянескольких возможных интерпретаций входящих в него идентификаторовили операций, то дальнейший анализ контекста не даст ощутимыхрезультатов, т.к.
не позволит отдать предпочтение какой-то одной изимеющихся интерпретаций. Следовательно, все эти интерпретации будутдопустимыми.Более формально для данной конструкции допустимые интерпретации(legal interpretation) вхождений идентификаторов или операций в точке ихиспользования находятся следующим образом:1. Если данная конструкция не имеет в своем составе другихконструкций, то рассматриваются все комбинации возможныхинтерпретаций идентификаторов и операций. В противном случаерассматриваются все комбинации интерпретаций, допустимых длясоставляющих конструкций.2.
Далее удаляются те комбинации, которые не удовлетворяютконтекстным условиям данной конструкции.3. В заключение, если конструкция представляет собой выражение,принадлежащее синтаксической категории value_expr, удаляются текомбинации, при которых максимальные типы данной конструкции неразличимы.Полученные в результате описанного процесса комбинации интерпретацийсодержат допустимые для данной конструкции интерпретации вхождений ееидентификаторов и операций.Перегрузка называется разрешимой (resolvable), если существует в точностиодна допустимая интерпретация каждого идентификатора и операции в егоближайшем объемлющем ‘разрешающем контексте’.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
