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

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

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

Аналогично, если:

• максимальный тип t₁ приводим к максимальному типу t₂,

• максимальный тип t₃ приводим к максимальному типу t₄,

• t₁ и t₃ не имеют наименьшей верхней границы,

• t₂ и t₄ имеют наименьшую верхнюю границу t,

• два выражения типов t₁ и t₃ соответственно встречаются в контексте, который требует, чтобы они имели наименьшую верхнюю границу.

Тогда говорят, что имеют место неявные приведения типов указанных двух выражений t₁ к t₂ и t₃ к t₄ соответственно. Эта формулировка может быть обобщена для набора произвольного количества выражений.

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

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

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

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

6.2. Литералы (Value Literals)

Синтаксис.

value_literal ::=

unit_literal 

bool_literal 

int_literal 

real_literal 

text_literal 

char_literal

unit_literal ::=

()

bool_literal ::=

true 

false

Значением метапеременной int_literal является любая непустая строка цифр. Значением метапеременной real_literal являются две непустые строки цифр, разделенные десятичной точкой. Метапеременная text_literal представляет собой текст (возможно, пустой) в двойных кавычках. Значением метапеременной char_literal является любой допустимый в RSL символ, взятый в апострофы.

Атрибуты. Максимальным типом unit_literal является Unit.

Максимальным типом bool_literal является Bool.

Максимальным типом int_literal является Int.

Максимальным типом real_literal является Real.

Максимальным типом text_literal является Char^.

Максимальным типом char_literal является Char.

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

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

Текстовый литерал вида "c₁ … c_n" представляет собой сокращенную запись выражения c₁, …,c_n.

6.3. Имена

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

Атрибуты. Максимальный тип имени name определен в разделе 10.

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

Семантика. См. раздел 10.

6.4. Пред-имена (Pre-names)

Синтаксис.

pre_name ::=

variable-name`

Контекст и правила видимости. Если в ближайшем объемлющем постусловии присутствуют какие-либо определения локальных переменных, они не видимы в данном имени name.

Контекстные условия. Выражение pre_name должно появляться внутри постусловия.

Имя name должно представлять некоторую переменную.

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

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

Семантика. Выражение pre_name встречается внутри постусловий (см. раздел 6.13.). Результирующее воздействие выражения pre_name состоит в том, чтобы вернуть содержание переменной, представленной именем name, в пред-состоянии (pre-state).

6.5. Базисные выражения (Basic Expressions)

Синтаксис.

basic_expr ::=

chaos 

skip 

stop 

swap

Атрибуты. Максимальным типом выражения skip является Unit. Максимальным типом выражений chaos, stop и swap может быть любой максимальный тип.

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

Семантика.

• Результирующее воздействие выражения chaos расходится.

• Результирующее воздействие выражения skip заключается в возвращении значения типа Unit.

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

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

6.6. Декартовы произведения (Product Expressions)

Синтаксис.

product_expr ::=

( value_expr-list2 )

Атрибуты. Максимальным типом выражения product_expr вида (value_expr₁,…, value_expr_n) является декартово произведение t₁ ´ … ´ t_n, где t₁, …, t_n являются соответственно максимальными типами выражений value_expr₁, …, value_expr_n.

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

Семантика. Результирующее воздействие выражения product_expr вида (value_expr₁,…, value_expr_n) состоит в вычислении слева направо значений v_i каждого составляющего выражения value_expr_i, после чего возвращается значение декартова произведения (v₁,…,v_n).

6.7. Множественные выражения (Set expressions)

Синтаксис.

set_expr ::=

ranged_set_expr ½

enumereted_set_expr ½

comprehended_set_expr

6.7.1. Множества, заданные диапазоном (Ranged Set Expressions)

Синтаксис.

ranged_set_expr ::=

{ readonly_integer-value_expr .. readonly_integer-value_expr }

Контекстные условия. Входящие в данную конструкцию выражения value_expr должны представлять собой read-only выражения и их максимальный тип должен быть Int.

Атрибуты. Максимальным типом выражения ranged_set_expr является Int‑infset.

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

Семантика. Результирующее воздействие выражения ranged_set_expr заключается в возвращении множества целых чисел в диапазоне, ограниченном нижней и верхней границами. При этом первое выражение value_expr вычисляется и возвращает нижнюю границу i₁, затем вычисляется второе выражение value_expr и возвращает верхнюю границу i₂. Результирующее множество содержит все целые числа i такие, что i₁  i  i₂. Если i₁  i₂, множество пусто.

6.7.2. Множества, заданные перечислением (Enumerated Set Expressions)

Синтаксис.

enumerated_set_expr ::=

{ readonly-opt-value_expr-list }

Контекстные условия. Входящие в данную конструкцию выражения value_expr должны представлять собой read-only выражения.

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

Атрибуты. Максимальным типом выражения enumerated_set_expr, имеющего в своем составе одно или более выражений value_expr, является t-infset, где t – это наименьшая верхняя граница максимальных типов этих составляющих выражений value_expr. Максимальным типом выражения enumerated_set_expr, не имеющего составляющих выражений value_expr (пустое множество), является t-infset, где t – это типовая переменная, представляющая произвольный максимальный тип.

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

Семантика. Результирующее воздействие выражения enumerated_set_expr заключается в возвращении множества явно специфицированных значений. При этом результирующее воздействие выражения enumerated_set_expr вида {value_expr₁,…, value_expr_n} достигается путем вычисления слева направо значений v_i каждого составляющего выражения value_expr_i, после чего возвращается значение в виде множества {v₁,…,v_n}. Если список value_expr‑list отсутствует, возвращается пустое множество.

6.7.3. Сокращенные множественные выражения (Comprehended Set Expressions)

Синтаксис.

comprehended_set_expr ::=

{ readonly-value_expr ½ set_limitation }

set_limitation ::=

typing-list opt-restriction

restriction ::=

• readonly_logical-value_expr

Контекстно-независимые расширения. Пустое ограничение nil‑restriction представляет собой сокращение ограничения ‘• true’.

Ограничение ‘• value_expr’ является сокращенной записью ограничения ‘• value_expr  true’.

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

Непосредственным контекстом конструкций typing, входящих в состав ограничения set_limitation, является ограничение restriction, входящее в тот же состав.

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

Входящее в состав ограничения restriction выражение value_expr должно представлять собой read-only выражение и его максимальный тип должен быть Bool.

Атрибуты. Максимальным типом выражения comprehended_set_expr является t-infset, где t – это максимальный тип входящего в его состав выражения value_expr.

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

Конструкция set_limitation, в которой присутствует ограничение restriction, статически производит доступ к тем переменным и каналам, к которым статически обращается данное ограничение restriction.

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

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

Для каждой модели из множества моделей, представленного ограничением set_limitation (см. ниже), вычисляется указанное выражение value_expr. Вычисление выражения comprehended_set_expr представляет собой сходящийся процесс.

Конструкция set_limitation представляет некоторое подмножество моделей, которые удовлетворяют определениям, заданным в списке typing-list, и для которых выполняется ограничение restriction.

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

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