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

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

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

равно true тогда и только тогда, когда:

• вычисление выражения value_expr₁ представляет собой сходящийся процесс;

• вычисление выражения value_expr₂ сходится, и его результат равен true при выполнении этого вычисления в пост-состоянии (post-state), которое является результатом вычисления выражения value_expr₁ в пред-состоянии (pre-state) и в контексте определений, полученных путем сопоставления возвращаемого выражением value_expr₁ значения со связыванием binding.

Внутри выражения value_expr₂ на значения переменных в пред-состоянии можно ссылаться путем добавления суффикса ` к именам соответствующих переменных (конструкция pre_name). Переменные пост-состояния доступны по своим обычным именам (без суффикса `).

Вычисление пост-выражения post_expr представляет собой сходящийся процесс.

6.14. Выражения со снятием неопределенности (Disambiguation Expressions)

Синтаксис.

disambiguation_expr ::=

value_expr : type_expr

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

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

Семантика. Результирующее воздействие выражения со снятием неопределенности disambiguation_expr совпадает с результирующим воздействием выражения value_expr.

6.15. Выражения в скобках (Bracketed Expressions)

Синтаксис.

bracketed_expr ::=

( value_expr )

Атрибуты. Максимальным типом выражения в скобках bracketed_expr является максимальный тип выражения value_expr.

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

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

6.16. Инфиксные выражения (Infix Expressions)

Синтаксис.

infix_expr ::=

stmt_infix_expr ½

axiom_infix_expr ½

value_infix_expr

6.16.1. Операторные инфиксные выражения (Statement Infix Expressions)

Синтаксис.

stmt_infix_expr ::=

value_expr infix_combinator value_expr

Контекстные условия. Для инфиксного комбинатора infix_combinator, являющегося:

▌ или : максимальные типы обоих выражений value_expr должны иметь наименьшую верхнюю границу.

║ или ╫: оба указанных выражения value_expr должны иметь максимальный тип Unit.

; : максимальный тип первого выражения value_expr должен быть Unit.

Атрибуты. Для инфиксного комбинатора infix_combinator, являющегося:

▌ или : максимальным типом операторного инфиксного выражения stmt_infix_expr является наименьшая верхняя граница максимальных типов составляющих его выражений value_expr.

║ или ╫: максимальным типом операторного инфиксного выражения stmt_infix_expr является тип Unit.

; : максимальным типом операторного инфиксного выражения stmt_infix_expr является максимальный тип второго входящего в него выражения value_expr.

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

Семантика. См. определение инфиксных комбинаторов infix_combinator (раздел 13).

6.16.2. Аксиоматические инфиксные выражения (Axiom Infix Expressions)

Синтаксис.

axiom_infix_expr ::=

logical-value_expr infix_connective logical-value_expr

Контекстные условия. Максимальным типом обоих указанных выражений value_expr должен быть тип Bool.

Контекстно-зависимые расширения. См. определение инфиксных связок infix_connective (раздел 12.1).

6.16.3. Инфиксные выражения (Value Infix Expressions)

Синтаксис.

value_infix_expr ::=

value_expr infix_op value_expr

Контекстные условия. Тип t₁ ´ t₂ , где t₁ и t₂ – это максимальные типы указанных двух выражений value_expr, должен быть меньше или равен параметрической части (часть, где задается тип параметров операции) максимального типа инфиксной операции infix_op.

Атрибуты. Максимальным типом инфиксного выражения value_infix_expr является результирующая часть (часть, где задается тип результата) максимального типа инфиксной операции infix_op.

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

Семантика. Результирующее воздействие инфиксного выражения value_infix_expr заключается в вычислении значения v₁ первого выражения value_expr и затем значения v₂ второго выражения value_expr, после чего возвращается результат применения функции, определяемой инфиксной операцией infix_op, к паре (v₁, v₂).

6.17. Префиксные выражения (Prefix Expressions)

Синтаксис.

prefix_expr ::=

axiom_prefix_expr ½

universal_prefix_expr ½

value_prefix_expr

6.17.1. Аксиоматические префиксные выражения (Axiom Prefix Expressions)

Синтаксис.

axiom_prefix_expr ::=

prefix_connective logical-value_expr

Контекстно-независимые расширения. См. определение префиксных связок prefix_connective (раздел 12.2).

6.17.2. Универсальные префиксные выражения (Universal Prefix Expressions)

Синтаксис.

universal_prefix_expr ::=

□ readonly_logical-value_expr

Контекстно-независимые расширения. Универсальное префиксное выражение universal_prefix_expr вида:

□ value_expr

эквивалентно выражению:

□ ( value_expr  true )

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

Выражение value_expr должно представлять собой read-only выражение.

Атрибуты. Максимальным типом универсального префиксного выражения universal_prefix_expr является тип Bool.

Универсальное префиксное выражение universal_prefix_expr не обращается статически ни к каким переменным или каналам.

Семантика. Универсальное префиксное выражение universal_prefix_expr вида:

□ value_expr

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

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

6.17.3. Префиксные выражения (Value Prefix Expressions)

Синтаксис.

value_prefix_expr ::=

prefix_op value_expr

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

Атрибуты. Максимальным типом префиксного выражения value_prefix_expr является результирующая часть максимального типа префиксной операции prefix_op.

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

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

6.18. Сокращенные выражения (Comprehended Expressions)

Синтаксис.

comprehended_expr ::=

associative_commutative-infix_combinator { value_expr ½ set_limitation }

Контекст и правила видимости. В сокращенном выражении comprehended_expr контекст ограничения set_limitation расширяется до выражения value_expr, входящего в состав данного выражения.

Контекстные условия. Инфиксный комбинатор infix_combinator должен обладать свойствами ассоциативности и коммутативности, т.е. он должен быть одним из следующих: ║, ▌, éê.

Для инфиксного комбинатора ║ максимальным типом выражения value_expr должен быть Unit.

Атрибуты. Максимальным типом сокращенного выражения comprehended_expr является максимальный тип входящего в его состав выражения value_expr.

Сокращенное выражение comprehended_expr статически производит доступ к тем переменным и каналам, к которым статически обращаются составляющие его выражение value_expr и ограничение set_limitation.

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

Данное множество содержит выражение value_expr для каждой модели из множества моделей, представленного ограничением set_limitation. Это выражение value_expr вычисляется в соответствующей модели и в конкретном текущем состоянии. Результирующим воздействием вычисления сокращенного выражения comprehended_expr является:

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

• результирующее воздействие от разрешения внутреннего выбора между результирующими воздействиями вычисления выражений value_expr в этих же моделях (в случае éê),

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

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

▌ {}  stop

éê {}  swap

║ {}  skip

6.19. Инициализирующие выражения (Initialise Expressions)

Синтаксис.

initialise_expr ::=

initialise

Атрибуты. Максимальным типом инициализирующего выражения initialise_expr является Unit.

Инициализирующее выражение initialise_expr статически производит запись во все переменные, инициализируемые этим выражением, и не обращается статически ни к каким каналам.

Семантика. Результирующее воздействие инициализирующего выражения initialise_expr состоит в том, чтобы присвоить переменным их начальные значения. Инициализирующее выражение initialise_expr возвращает Unit значение. Начальное значение переменной может быть задано явно в определении этой переменной; если оно там явно не задано, то, тем не менее, существует некоторое определенное значение, которое всегда присваивается данной переменной инициализирующим выражением initialise_expr.

С помощью данного выражения инициализируются все переменные, определенные доступом ‘any’ (см. раздел 5.11).

6.20. Выражения присваивания (Assignment Expressions)

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

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