rsl.formal.specifications.conspect (811084), страница 12
Текст из файла (страница 12)
Результирующее воздействие квантифицированного выраженияquantified_expr заключается в возвращении булевского значения, зависящегоот значения, которое возвращает некоторый предикат для каждой модели изнекоторого множества моделей. Моделями, о которых идет речь, являютсявсе модели, удовлетворяющие определениям, представленным указаниямитипа typing-list.Если в качестве квантора quantifier используется ∀, возвращаемое значениеравно true тогда и только тогда, когда ограничение restriction выполняется длявсех рассматриваемых моделей. Если квантором quantifier является ∃,возвращаемое значение равно true тогда и только тогда, когда ограничениеrestriction выполняется по крайней мере для одной рассматриваемой модели.И, наконец, если в качестве квантора quantifier используется ∃!, возвращаемоезначение равно true тогда и только тогда, когда ограничение restrictionвыполняется в точности для одной рассматриваемой модели.Вычисление квантифицированного выражения quantified_expr представляетсобой сходящийся процесс.6.12.
Выражения эквивалентности (Equivalence Expressions)Синтаксис.equivalence_expr ::=value_expr ≡ value_expr opt-pre_conditionpre_condition ::=pre readonly_logical-value_exprКонтекстные условия. Максимальные типы входящих в даннуюконструкцию выражений value_expr должны иметь наименьшую верхнююграницу.Выражение value_expr, входящее в состав предусловия pre_condition, должнопредставлять собой read-only выражение и его максимальный тип долженбыть Bool.Контекстно-зависимыерасширения.Выражениеэквивалентностиequivalence_expr вида:value_expr1 ≡ value_expr2 pre value_expr361представляет собой сокращенную форму выражения:( value_expr3 ≡ true ) ⇒ value_expr1 ≡ value_expr2Атрибуты.Максимальнымтипомвыраженияэквивалентностиequivalence_expr является Bool.Предусловие pre_condition статически производит чтение из тех переменных,из которых статически производит чтение составляющее его выражениеvalue_expr, и не обращается статически ни к каким каналам.Выражение эквивалентности equivalence_expr статически производит чтениетех переменных, к которым статически обращаются по чтению или записивходящие в него выражения value_expr.
Оно также статически производитчтение переменных, из которых статически осуществляет чтениепредусловие pre_condition (в случае его присутствия). Выражениеэквивалентности equivalence_expr не обращается статически ни к какимканалам.Семантика. Результирующее воздействие выражения эквивалентностиequivalence_expr заключается в возвращении некоторого булевского значения,зависящего от того, обладают ли два входящих в него выражения value_exprодинаковым результирующим воздействием при вычислении каждого из нихв текущем состоянии.
Результирующие воздействия указанных двухвыражений value_expr используются только для определения этогобулевского значения и игнорируются в дальнейшем.Значение, возвращаемое выражением эквивалентности equivalence_expr вида:value_expr1 ≡ value_expr2равно true тогда и только тогда, когда выражение value_expr1, вычисленное втекущем состоянии, представляет в точности такое же результирующеевоздействие, что и выражение value_expr2 , вычисленное в том же состоянии.Это означает, что указанные два выражения value_expr должны представлятьодно и то же результирующее воздействие в отношении возвращаемыхзначений, изменений состояния, предложений взаимодействия, внешнихвыборов, тупиковых ситуаций, внутренних выборов и расходимости.Вычисление выражения эквивалентности equivalence_expr представляетсобой сходящийся процесс.6.13. Пост-выражения (Post-expressions)Синтаксис.post_expr ::=value_expr post_condition opt-pre_conditionpost_condition ::=opt-result_naming post readonly_logical-value_expr62result_naming ::=as bindingКонтекст и правила видимости.
В постусловии post_condition контекстомконструкции opt-result_naming является выражение value_expr.Контекстные условия. В постусловии post_condition входящее в неговыражение value_expr должно представлять собой read-only выражение и егомаксимальный тип должен быть Bool.Контекстно-зависимые расширения. Пост-выражение post_expr вида:value_expr1 post value_expr2представляет собой сокращенную запись выражения:value_expr1 as id post value_expr2где id - это некоторый идентификатор уже вне контекста.Пост-выражение post_expr вида:value_expr1 post_condition pre value_expr2представляет собой сокращенную запись выражения:( value_expr2 ≡ true ) ⇒ value_expr1 post_conditionАтрибуты.
Максимальным типом пост-выражения post_expr является Bool.Контекст постусловия post_condition определяет максимальный контекстныйтип данного постусловия post_condition.В пост-выражении post_expr максимальным контекстным типом постусловияpost_condition является максимальный тип составляющего его выраженияvalue_expr.В конструкции result_naming максимальным контекстным типом связыванияbinding является максимальный контекстный тип ближайшего объемлющегопостусловия.Пост-выражение post_expr статически производит чтение тех переменных, ккоторым статически обращается по чтению или записи входящее в неговыражение value_expr.
Оно также статически производит чтение переменных,из которых статически осуществляет чтение предусловие pre_condition (вслучае его присутствия). Пост-выражение post_expr не обращаетсястатически ни к каким каналам.Семантика. Результирующее воздействие пост-выражения post_exprзаключается в возвращении некоторого булевского значения, котороезависит от результирующего воздействия выражения value_expr,вычисленного в пред-состоянии (pre-state). Результирующее воздействиевыражения value_expr используется только для определения этого булевскогозначения и игнорируется в дальнейшем.Значение, возвращаемое пост-выражением post_expr вида:value_expr1 as binding post value_expr263равно true тогда и только тогда, когда:• вычисление выражения value_expr1 представляет собой сходящийсяпроцесс;• вычисление выражения value_expr2 сходится, и его результат равен trueпри выполнении этого вычисления в пост-состоянии (post-state),которое является результатом вычисления выражения value_expr1 впред-состоянии (pre-state) и в контексте определений, полученныхпутем сопоставления возвращаемого выражением value_expr1 значениясо связыванием binding.Внутри выражения value_expr2 на значения переменных в пред-состоянииможно ссылаться путем добавления суффикса ` к именам соответствующихпеременных (конструкция pre_name).
Переменные пост-состояния доступныпо своим обычным именам (без суффикса `).Вычисление пост-выражения post_expr представляет собой сходящийсяпроцесс.6.14. Выражения со снятием неопределенности (DisambiguationExpressions)Синтаксис.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.64Выражение в скобках bracketed_expr статически производит доступ к темпеременным и каналам, к которым статически обращается составляющее еговыражение value_expr.Семантика. Результирующее воздействие выражения в скобкахbracketed_expr совпадает с результирующим воздействием входящего в егосостав выражения value_expr.6.16. Инфиксные выражения (Infix Expressions)Синтаксис.infix_expr ::=stmt_infix_expr ⏐axiom_infix_expr ⏐value_infix_expr6.16.1.
Операторные инфиксные выражения (Statement InfixExpressions)Синтаксис.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).656.16.2. Аксиоматические инфиксные выражения (Axiom InfixExpressions)Синтаксис.axiom_infix_expr ::=logical-value_expr infix_connective logical-value_exprКонтекстные условия. Максимальным типом обоих указанных выраженийvalue_expr должен быть тип Bool.Контекстно-зависимые расширения. См. определение инфиксных связокinfix_connective (раздел 12.1).6.16.3.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
