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

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

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

5.11. Описания доступа (Access Descriptions)

Синтаксис.

access_desc ::=

access_mode access-list

access_mode ::=

read ½

write ½

in ½

out

access ::=

variable_or_channel-name ½

enumerated_access ½

completed_access ½

comprehended_access

enumerated_access ::=

{ opt-access-list }

completed_access ::=

any

comprehended_access ::=

{ access ½ pure-set_limitation }

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

Статический доступ – это множество переменных или множество каналов.

Контекст и правила видимости. В конструкции comprehended_access контекст ограничения set_limitation расширяется до конструкции access.

Контекстные условия. Если значением метапеременной access является имя name, это имя должно представлять:

• переменную, если оно появляется в списке access-list описания access_desc со значениями read или write в качестве режима доступа access_mode;

• канал, если оно появляется в списке access-list описания access_desc со значениями in или out в качестве режима доступа access_mode.

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

Атрибуты. С описаниями opt-access_desc-string и access_desc связаны четыре описания статического доступа: описание статического доступа по чтению, описание статического доступа по записи, описание статического доступа по вводу и описание статического доступа по выводу.

Для пустой строки описания nil-access_desc-string описание статического доступа по чтению, записи, вводу и выводу являются пустыми.

Для строки access_desc-string описание статического доступа по чтению представляет собой объединение описаний статического доступа по чтению всех входящих в данную строку описаний access_desc. Аналогично для описаний доступа по записи, вводу и выводу.

Для описания access_desc с режимом доступа read описание статического доступа по чтению равно объединению статических доступов его составляющих access, тогда как его описания статического доступа по записи, вводу и выводу пусты. Аналогично для описания access_desc с режимом доступа in или out. Для описания access_desc с режимом доступа write описания статического доступа по чтению и по записи оба равны объединению статических доступов его составляющих access, тогда как его описания статического доступа по вводу и выводу пусты.

С каждой конструкцией access ассоциируется некоторый статический доступ.

Для имени name, представляющего собой некоторый идентификатор, статическим доступом является множество, которое содержит в качестве своего единственного элемента переменную или канал, представленную данным идентификатором.

Статическим доступом перечисления enumerated_access является пустое множество в случае отсутствия составляющих его элементов access, в противном случае статический доступ перечисления представляет собой объединение статических доступов входящих в него конструкций access.

Статическим доступом конструкции completed_access вида any является множество всех переменных или каналов, которые определены в ближайшем объемлющем данную конструкцию классовом выражении или которые могли быть определены в любом расширении этого классового выражения.

Статическим доступом конструкции comprehended_access является статический доступ входящей в нее конструкции access.

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

Описания доступа opt-access_desc-string и access_desc представляют четыре множества переменных и каналов:

• множество переменных с режимом доступа access_mode равным read, из которых может осуществляться чтение, — множество чтения;

• множество переменных с режимом доступа access_mode равным write, в которые может осуществляться запись (т.е. они могут изменяться за счет присваивания), — множество записи; переменные с режимом доступа write автоматически имеют режим доступа read;

• множество каналов с режимом доступа access_mode равным in, по которым может осуществляться ввод, — множество ввода;

• множество каналов с режимом доступа access_mode равным out, по которым может осуществляться вывод, — множество вывода.

Для пустой строки описания nil-access_desc-string множества чтения, записи, ввода и вывода являются пустыми.

Для строки access_desc-string множество чтения представляет собой объединение множеств чтения всех составляющих ее описаний access_desc. Аналогичное утверждение справедливо для множеств записи, ввода и вывода.

Для описания access_desc с режимом доступа read множество чтения равно объединению множеств всех составляющих его конструкций access, тогда как его множества записи, ввода и вывода пусты. Аналогично для описания access_desc с режимом доступа in или out.

Для описания access_desc с режимом доступа write множество чтения и множество записи равны объединению множеств всех составляющих его конструкций access, тогда как его множества ввода и вывода пусты.

Конструкция access представляет некоторое множество переменных или каналов.

Множество, представленное именем name, содержит в качестве своего единственного элемента переменную или канал с данным именем.

Множество, представленное перечислением enumerated_access, является пустым в случае отсутствия составляющих это перечисление элементов access, в противном случае оно представляет собой объединение множеств составляющих данное перечисление конструкций access.

Множеством, представленным конструкцией completed_access вида any, является множество всех переменных или каналов, которые определены в ближайшем объемлющем данную конструкцию классовом выражении или которые могли быть определены в любом расширении этого классового выражения.

Конструкция comprehended_access представляет собой следующее множество. Для каждой модели из множества моделей, заданного ограничением set_limitation, составляющая access представляет некоторое конкретное множество. Объединение всех таких множеств и образует искомое множество.

1. Value Expressions (выражения)

6.1. Общие замечания

Синтаксис.

value_expr ::=

value_literal 

value_or_variable-name 

pre_name 

basic_expr 

product_expr 

set_expr 

list_expr 

map_expr 

function_expr 

application_expr 

quantified_expr 

equivalence_expr 

post_expr 

disambiguation_expr 

bracketed_expr 

infix_expr 

prefix_expr 

comprehended_expr 

initialise_expr 

assignment_expr 

input_expr 

output_expr 

structured_expr

Терминология. Выражение value_expr вычисляется (выполняется) в контексте некоторого набора определений и в некотором состоянии. Иногда используется терминология, что выражение value_expr вычисляется ‘в некоторой модели’ (имея в виду модель, удовлетворяющую заданным определениям) и в некотором состоянии. Часто говорят, что выражение value_expr вычисляется, не упоминая при этом какого-либо конкретного набора определений или какого-либо конкретного состояния. Однако такие сокращения могут быть использованы только в тех ситуациях, когда соответствующий набор определений или состояние однозначным образом задаются контекстом изложения, и, следовательно, подобные сокращения не могут привести к путанице.

Результирующее воздействие (effect) выражения value_expr на некоторое состояние заключается в вычислении этого выражения в данном состоянии, после чего оно может:

• вернуть некоторое значение;

• произвести доступ к переменным путем чтения или записи;

• предложить произвести доступ к каналам для ввода или вывода.

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

1. возможно, после изменения данного состояния завершиться возвратом некоторого значения;

2. возможно, после изменения данного состояния предложить осуществить взаимодействие путем ожидания ввода из канала или вывода в канал и продолжиться с дальнейшим результирующим воздействием;

3. разрешить внешний выбор между эффектами, подпадающими под категории 1 или 2;

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

5. разрешить внутренний выбор между эффектами, подпадающими под категории 3 или 4;

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

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

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

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

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

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

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

Говорят, что выражение value_expr статически производит доступ к переменной (статически обращается к переменной), если оно статически производит чтение или запись в эту переменную. Выражение value_expr статически производит доступ к каналу (статически обращается к каналу), если оно статически производит ввод или вывод по этому каналу.

Выражение value_expr называется чистым, если оно не производит статически доступа к какой-либо переменной или каналу.

Выражение value_expr называется read-only (доступным только для чтения), если оно не производит статически запись в какую-либо переменную и не производит статически доступ к какому-либо каналу.

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

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

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