rsl.formal.specifications.conspect (811084), страница 10
Текст из файла (страница 10)
Базисные выражения (Basic Expressions)Синтаксис.basic_expr ::=chaos ⏐skip ⏐stop ⏐swapАтрибуты. Максимальным типом выражения skip является Unit.Максимальным типом выражений chaos, stop и swap может быть любоймаксимальный тип.Выражение basic_expr не производит статически доступа к каким-либопеременным или каналам.Семантика.• Результирующее воздействие выражения chaos расходится.• Результирующее воздействие выражения skip заключается ввозвращении значения типа Unit.50• Результирующим воздействием выражения stop является тупиковаяситуация.• Результирующее воздействие выражения swap не специфицируется;это может быть завершение, переход в тупиковую ситуацию,разрешение внутреннего выбора или расходящийся процесс.6.6.
Декартовы произведения (Product Expressions)Синтаксис.product_expr ::=( value_expr-list2 )Атрибуты. Максимальным типом выражения product_expr вида(value_expr1,…, value_exprn) является декартово произведение t1 × … × tn, где t1,…, tn являются соответственно максимальными типами выраженийvalue_expr1, …, value_exprn.Выражение product_expr статически производит доступ к тем переменным иканалам, к которым статически обращаются составляющие его выраженияvalue_expr.Семантика. Результирующее воздействие выражения product_expr вида(value_expr1,…, value_exprn) состоит в вычислении слева направо значений viкаждого составляющего выражения value_expri, после чего возвращаетсязначение декартова произведения (v1,…,vn).6.7.
Множественные выражения (Set expressions)Синтаксис.set_expr ::=ranged_set_expr ⏐enumereted_set_expr ⏐comprehended_set_expr6.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.51Выражение ranged_set_expr статически производит чтение из техпеременных, из которых статически производят чтение составляющие еговыражения value_expr, и не имеет другого статического доступа.Семантика.
Результирующее воздействие выражения ranged_set_exprзаключается в возвращении множества целых чисел в диапазоне,ограниченном нижней и верхней границами. При этом первое выражениеvalue_expr вычисляется и возвращает нижнюю границу i1, затем вычисляетсявторое выражение value_expr и возвращает верхнюю границу i2.Результирующее множество содержит все целые числа i такие, что i1 ≤ i ≤ i2.Если i1 > i2, множество пусто.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_expr1,…, value_exprn} достигается путем вычисления слева направозначений vi каждого составляющего выражения value_expri, после чеговозвращается значение в виде множества {v1,…,vn}. Если списокvalue_expr-list отсутствует, возвращается пустое множество.526.7.3.
Сокращенные множественные выражения (Comprehended SetExpressions)Синтаксис.comprehended_set_expr ::={ readonly-value_expr ⏐ set_limitation }set_limitation ::=typing-list opt-restrictionrestriction ::=• 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 во всех моделях, удовлетворяющихзаданному ограничению.53Для каждой модели из множества моделей, представленного ограничениемset_limitation (см. ниже), вычисляется указанное выражение value_expr.Вычисление выражения comprehended_set_expr представляет собойсходящийся процесс.Конструкция set_limitation представляет некоторое подмножество моделей,которые удовлетворяют определениям, заданным в списке typing-list, и длякоторых выполняется ограничение restriction.Ограничение restriction выполняется, если вычисление входящего в его составвыражения value_expr представляет собой сходящийся процесс, в результатекоторого возвращается значение true.6.8. Выражения, задающие списки (List expressions)Синтаксис.list_expr ::=ranged_list_expr ⏐enumereted_list_expr ⏐comprehended_list_expr6.8.1.
Списки, заданные диапазоном (Ranged List Expressions)Синтаксис.ranged_list_expr ::=〈 integer-value_expr .. integer-value_expr 〉Контекстные условия. Максимальным типом входящих в даннуюконструкцию выражений value_expr должен быть Int.Атрибуты. Максимальным типом выражения ranged_list_expr является Intω.Выражение ranged_list_expr статически производит доступ к тем переменными каналам, к которым статически обращаются составляющие его выраженияvalue_expr.Семантика. Результирующее воздействие выражения ranged_list_exprзаключается в возвращении списка целых чисел в диапазоне, ограниченномнижней и верхней границами.
При этом вычисляется первое выражениеvalue_expr и возвращает нижнюю границу i1, затем вычисляется второевыражение value_expr и возвращает верхнюю границу i2. Результирующийсписок содержит в возрастающем порядке все целые числа i такие, чтоi1 ≤ i ≤ i2. Если i1 > i2, список пуст.6.8.2. Списки, заданные перечислением (Enumerated List Expressions)Синтаксис.enumerated_list_expr ::=〈 opt-value_expr-list 〉54Контекстные условия. Максимальные типы составляющих даннуюконструкцию выражений value_expr должны иметь наименьшую верхнююграницу.Атрибуты.
Максимальным типом выражения enumerated_list_expr, имеющегов своем составе одно или более выражений value_expr, является tω, где t – этонаименьшая верхняя граница максимальных типов этих составляющихвыражений value_expr.Максимальным типом выражения enumerated_list_expr, не имеющего в своемсоставе выражений value_expr (пустой список), является tω, где t – этотиповая переменная, представляющая произвольный максимальный тип.Выражение enumerated_list_expr статически производит доступ к темпеременным и каналам, к которым статически обращаются составляющиеего выражения value_expr.Семантика.
Результирующее воздействие выражения enumerated_list_exprзаключается в возвращении списка явно специфицированных значений. Приэтом результирующее воздействие выражения enumerated_list_expr вида〈value_expr1,…, value_exprn〉 достигается путем вычисления слева направозначений vi каждого выражения value_expri, после чего возвращаетсязначение в виде списка 〈v1,…,vn〉. Если конструкция value_expr-listотсутствует, возвращается пустой список.6.8.3.
Сокращенные выражения для списков (Comprehended ListExpressions)Синтаксис.comprehended_list_expr ::=〈 value_expr ⏐ list_limitation 〉list_limitation ::=binding in readonly_list-value_expr opt-restrictionКонтекст и правила видимости. В выражении comprehended_list_exprконтекст ограничения list_limitation расширяется до выражения value_expr,входящего в состав данного выражения.Непосредственным контекстом конструкции binding, входящей в составограничения list_limitation, является ограничение restriction, входящее в тот жесостав.Контекстные условия. Входящее в состав ограничения list_limitationвыражение value_expr должно представлять собой read-only выражение и егомаксимальный тип должен быть типом список.Атрибуты. Максимальным типом выражения comprehended_list_expr являетсяtω, где t – это максимальный тип входящего в его состав выраженияvalue_expr.55В конструкции list_limitation максимальным контекстным типом связыванияωbinding является t, где t – это максимальный тип входящего в состав даннойконструкции выражения value_expr.Выражение comprehended_list_expr статически производит доступ к темпеременным и каналам, к которым статически обращаются составляющиеего выражение value_expr и ограничение set_limitation.Конструкция list_limitation статически производит чтение из тех жепеременных, что и входящее в ее состав выражение value_expr.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
