rsl.formal.specifications.conspect (811084), страница 13
Текст из файла (страница 13)
Инфиксные выражения (Value Infix Expressions)Синтаксис.value_infix_expr ::=value_expr infix_op value_exprКонтекстные условия. Тип t1 × t2 , где t1 и t2 – это максимальные типыуказанных двух выражений value_expr, должен быть меньше или равенпараметрической части (часть, где задается тип параметров операции)максимального типа инфиксной операции infix_op.Атрибуты. Максимальным типом инфиксного выражения value_infix_exprявляется результирующая часть (часть, где задается тип результата)максимального типа инфиксной операции infix_op.Инфиксное выражение value_infix_expr статически производит доступ к темпеременным и каналам, к которым статически обращаются составляющиеего выражения value_expr, а также к переменным и каналам, к которымстатически обращается тело соответствующей функции согласно описаниямстатического доступа максимального типа инфиксной операции infix_op.Семантика. Результирующее воздействие инфиксного выраженияvalue_infix_expr заключается в вычислении значения v1 первого выраженияvalue_expr и затем значения v2 второго выражения value_expr, после чеговозвращается результат применения функции, определяемой инфикснойоперацией infix_op, к паре (v1, v2).6.17.
Префиксные выражения (Prefix Expressions)Синтаксис.prefix_expr ::=axiom_prefix_expr ⏐universal_prefix_expr ⏐value_prefix_expr666.17.1. Аксиоматические префиксные выражения (Axiom PrefixExpressions)Синтаксис.axiom_prefix_expr ::=prefix_connective logical-value_exprКонтекстно-независимые расширения. См. определение префиксныхсвязок prefix_connective (раздел 12.2).6.17.2. Универсальные префиксные выражения (Universal PrefixExpressions)Синтаксис.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представляет собой сходящийся процесс.676.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 заключается в применении инфиксного комбинатора68и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║ {} ≡ skip6.19. Инициализирующие выражения (Initialise Expressions)Синтаксис.initialise_expr ::=initialiseАтрибуты.Максимальным типом инициализирующего выраженияinitialise_expr является Unit.Инициализирующее выражение initialise_expr статически производит записьво все переменные, инициализируемые этим выражением, и не обращаетсястатически ни к каким каналам.Семантика. Результирующее воздействие инициализирующего выраженияinitialise_expr состоит в том, чтобы присвоить переменным их начальныезначения. Инициализирующее выражение initialise_expr возвращает Unitзначение.
Начальное значение переменной может быть задано явно вопределении этой переменной; если оно там явно не задано, то, тем не менее,69существует некоторое определенное значение, которое всегда присваиваетсяданной переменной инициализирующим выражением initialise_expr.С помощью данного выражения инициализируются все переменные,определенные доступом ‘any’ (см.
раздел 5.11).6.20. Выражения присваивания (Assignment Expressions)Синтаксис.assignment_expr ::=variable-name := value_exprКонтекстные условия. Имя name должно представлять некоторуюпеременную.Максимальный тип выражения value_expr должен быть меньше или равенмаксимального типа имени name.Атрибуты. Максимальным типом выражения присваивания assignment_exprявляется Unit.Выражение присваивания assignment_expr статически производит запись впеременную, представленную входящим в его состав именем name, а такжестатически производит доступ к переменным или каналам, к которымстатически обращается выражение value_expr.Семантика.
Результирующее воздействие выражения присваиванияassignment_expr состоит в том, чтобы записать (присвоить) значениевыражения value_expr в переменную, представленную именем name.Значением, возвращаемым выражением присваивания assignment_expr,является Unit значение.6.21. Input-выражения (Input Expressions)Синтаксис.input_expr ::=channel-name ?Контекстные условия. Имя name должно представлять некоторый канал.Атрибуты.
Максимальным типом input-выражения input_expr являетсямаксимальный тип входящего в его состав имени name.Выражение input_expr статически производит ввод по каналу,представленному именем name, и не обращается статически ни к какимпеременным.Семантика. Результирующее воздействие выражения input_expr состоит втом, чтобы предложить ввести данные по каналу, представленномууказанным именем name. Значением, возвращаемым выражением input_expr,является значение, введенное по указанному каналу, в случае, если70предложение произвести ввод совпадет с параллельным предложениемпроизвести вывод по тому же каналу.6.22. Output-выражения (Output Expressions)Синтаксис.output_expr ::=channel-name ! value_exprКонтекстные условия.
Имя name должно представлять некоторый канал.Максимальный тип выражения value_expr должен быть меньше или равенмаксимального типа имени name.Атрибуты. Максимальным типом output-выражения output_expr являетсяUnit.Выражение output_expr статически производит вывод по каналу,представленному входящим в его состав именем name, а также статическиобращается к переменным или каналам, к которым статически производитдоступ выражение value_expr.Семантика. Результирующее воздействие выражения output_expr состоит втом, чтобы предложить вывести данные по каналу, представленномууказанным именем name.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
