rsl.formal.specifications.conspect (811084), страница 9
Текст из файла (страница 9)
Аналогично для описанияaccess_desc с режимом доступа in или out.Для описания access_desc с режимом доступа write множество чтения имножество записи равны объединению множеств всех составляющих егоконструкций access, тогда как его множества ввода и вывода пусты.Конструкция access представляет некоторое множество переменных иликаналов.44Множество, представленное именем name, содержит в качестве своегоединственного элемента переменную или канал с данным именем.Множество, представленное перечислением enumerated_access, являетсяпустым в случае отсутствия составляющих это перечисление элементовaccess, в противном случае оно представляет собой объединение множествсоставляющих данное перечисление конструкций access.Множеством, представленным конструкцией completed_access вида any,является множество всех переменных или каналов, которые определены вближайшем объемлющем данную конструкцию классовом выражении иликоторые могли быть определены в любом расширении этого классовоговыражения.Конструкция comprehended_access представляет собой следующеемножество.
Для каждой модели из множества моделей, заданногоограничением set_limitation, составляющая access представляет некотороеконкретное множество. Объединение всех таких множеств и образуетискомое множество.6. Value Expressions (выражения)6.1. Общие замечанияСинтаксис.value_expr ::=value_literal ⏐value_or_variable-name ⏐pre_name ⏐basic_expr ⏐product_expr ⏐set_expr ⏐list_expr ⏐map_expr ⏐function_expr ⏐application_expr ⏐quantified_expr ⏐equivalence_expr ⏐post_expr ⏐disambiguation_expr ⏐bracketed_expr ⏐infix_expr ⏐prefix_expr ⏐comprehended_expr ⏐initialise_expr ⏐assignment_expr ⏐input_expr ⏐output_expr ⏐structured_expr45Терминология. Выражение value_expr вычисляется (выполняется) вконтексте некоторого набора определений и в некотором состоянии.Иногда используется терминология, что выражение value_exprвычисляется ‘в некоторой модели’ (имея в виду модель,удовлетворяющую заданным определениям) и в некотором состоянии.Часто говорят, что выражение value_expr вычисляется, не упоминая приэтом какого-либо конкретного набора определений или какого-либоконкретного состояния.
Однако такие сокращения могут бытьиспользованы только в тех ситуациях, когда соответствующий наборопределений или состояние однозначным образом задаются контекстомизложения, и, следовательно, подобные сокращения не могут привести кпутанице.Результирующее воздействие (effect) выражения value_expr на некотороесостояние заключается в вычислении этого выражения в данномсостоянии, после чего оно может:• вернуть некоторое значение;• произвести доступ к переменным путем чтения или записи;• предложить произвести доступ к каналам для ввода или вывода.Более формально результирующее воздействие выражения value_expr нанекоторое состояние состоит в том, чтобы выполнить одно из следующихдействий:1.
возможно, после изменения данного состояния завершиться возвратомнекоторого значения;2. возможно, после изменения данного состояния предложитьосуществить взаимодействие путем ожидания ввода из канала иливывода в канал и продолжиться с дальнейшим результирующимвоздействием;3.
разрешить внешний выбор между эффектами, подпадающими подкатегории 1 или 2;4. попасть в тупиковую ситуацию путем останова (в таком случае любойвнешний выбор между указанным эффектом и некоторым другимсводится к этому самому другому эффекту);5. разрешить внутренний выбор между эффектами, подпадающими подкатегории 3 или 4;6. разойтись путем продолжения вычисления без завершения, безпредложения осуществить взаимодействие и без тупиковой ситуации(в таком случае любой внешний или внутренний выбор между даннымрезультирующим воздействием и каким-либо другим такжерасходится).Результирующее воздействие является недетерминированным, если онодопускает внутренний выбор между другими результирующимивоздействиями. В подобных обстоятельствах, в частности, можетсуществовать более одного значения, которое может вернуть выражение, и46более одного изменения состояния, которое может достигаться при еговычислении.Будем говорить, что результирующее воздействие выражения value_expr нанекоторое состояние сходится, если выполнены следующие условия:• это результирующее воздействие не разрешает внутренний выбормежду каким-либо результирующим воздействием и тупиковойситуацией (т.е., в частности, оно не может расходиться или бытьтупиком);• это результирующее воздействие не разрешает внутренний выбормежду каким-либо результирующим воздействием и неким другимрезультирующим воздействием, завершающимся без предложениявзаимодействия (поэтому, в частности, если оно может завершиться, тооно завершается, и при этом существует единственное возвращаемоезначение и достигается единственное изменение состояния).Если в выражение value_expr входит несколько составляющих его выраженийvalue_expr, то должен быть установлен порядок их вычисления; обычно онивычисляются слева направо.
Порядок вычислений имеет значение в техслучаях, когда составляющие выражения value_expr производят запись впеременные, взаимодействуют по каналам или попадают в тупиковуюситуацию.Для выражений с описанным доступом используется следующаятерминология. Говорят, что выражение value_expr статически производитчтение (из) переменных своего описания статического доступа по чтению,статически производит запись в переменные своего описания статическогодоступа по записи, статически производит ввод из каналов своего описаниястатического доступа по вводу и статически производит вывод в каналысвоего описания статического доступа по выводу.Говорят, что выражение value_expr статически производит доступ кпеременной (статически обращается к переменной), если оно статическипроизводит чтение или запись в эту переменную.
Выражение value_exprстатически производит доступ к каналу (статически обращается кканалу), если оно статически производит ввод или вывод по этому каналу.Выражение value_expr называется чистым, если оно не производитстатически доступа к какой-либо переменной или каналу.Выражение value_expr называется read-only (доступным только для чтения),если оно не производит статически запись в какую-либо переменную и непроизводит статически доступ к какому-либо каналу.Предположим, имеется однозначное потенциальное приведение (см.
раздел5.1.) типа t1 к типу t2, т.е. тип t1 приводим к типу t2. Тогда, если некотороевыражение имеет максимальный тип t1 и встречается в контексте,требующим чтобы оно имело максимальный тип t, подтипом которогоявляется тип t2, говорят, что имеет место неявное приведение типа t1 к типу t2,представляющее собой применение указанного потенциального приведения(из t1 к t2) к данному выражению. Заметим, что в данных обстоятельствах t147меньше или равен t, поэтому неявное приведение типов (которое можетпредставлять собой применение тождественной функции) имеет местовсякий раз, когда контекстное условие требует, чтобы максимальный типвыражения был меньше или равен другого типа. Подобное неявноеприведение типа имеет место и для образцов (см.
раздел 9.1.).Аналогично, если:• максимальный тип t1 приводим к максимальному типу t2,• максимальный тип t3 приводим к максимальному типу t4,• t1 и t3 не имеют наименьшей верхней границы,• t2 и t4 имеют наименьшую верхнюю границу t,• два выражения типов t1 и t3 соответственно встречаются в контексте,который требует, чтобы они имели наименьшую верхнюю границу.Тогда говорят, что имеют место неявные приведения типов указанных двухвыражений t1 к t2 и t3 к t4 соответственно.
Эта формулировка может бытьобобщена для набора произвольного количества выражений.Контекстные условия. Неявные приведения типов должны бытьоднозначными.Контекстно-зависимые расширения. Выражение, для которого существуетнеявное приведение типов, не являющееся тождественной функцией,представляет собой краткую запись выражения, полученного путемприменения данного приведения типов.Атрибуты. С выражением value_expr ассоциируется некоторыймаксимальный тип (такой, что если выражение value_expr завершается, то егозначение принадлежит этому максимальному типу). С выражениемvalue_expr связаны также четыре описания статического доступа: описаниестатического доступа по чтению, описание статического доступа по записи,описание статического доступа по вводу и описание статического доступа повыводу.
Эти описания статического доступа таковы, что выражениеvalue_expr статически производит чтение некоторой переменной, еслирезультирующее воздействие данного выражения заключается впотенциальном чтении этой переменной, аналогично для записи, ввода ивывода.Для каждой конкретной разновидности выражения value_expr нижеопределены соответствующие максимальные типы и описания статическогодоступа.486.2. Литералы (Value Literals)Синтаксис.value_literal ::=unit_literal ⏐bool_literal ⏐int_literal ⏐real_literal ⏐text_literal ⏐char_literalunit_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заключается в возвращении значения, представленного указаннымлитералом.Текстовый литерал вида "c1 … cn" представляет собой сокращенную записьвыражения 〈′c1′, …,′cn′〉.6.3. ИменаКонтекстные условия.
Для выражения value_expr, являющегося именемname, это имя должно представлять какое-либо значение или переменную.Атрибуты. Максимальный тип имени name определен в разделе 10.Имя name, представляющее некоторое значение, не производит статическидоступа к каким-либо переменным или каналам. Имя name, представляющее49переменную, статически производит чтение из этой переменной и не имеетдругого статического доступа.Семантика. См. раздел 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.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
