Главная » Просмотр файлов » Языки и методы формальной спецификации

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

Файл №1158803 Языки и методы формальной спецификации (Языки и методы формальной спецификации) 13 страницаЯзыки и методы формальной спецификации (1158803) страница 132019-09-18СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

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

Синтаксис.

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, является значение, введенное по указанному каналу, в случае, если предложение произвести ввод совпадет с параллельным предложением произвести вывод по тому же каналу.

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. Предлагаемым для вывода значением является значение, возвращаемое выражением value_expr. Выражение output_expr возвращает Unit значение в случае, если предложение произвести вывод совпадет с параллельным предложением произвести ввод по тому же каналу.

6.23. Составные выражения (Structured Expressions)

Синтаксис.

structured_expr ::=

local_expr ½

let_expr ½

if_expr ½

case_expr ½

while_expr ½

until_expr ½

for_expr

6.23.1. Локальные выражения (Local Expressions)

Синтаксис.

local_expr ::=

local opt-decl-string in value_expr end

Контекст и правила видимости. Контекстом объявления opt-decl-string является само это объявление opt-decl-string и выражение value_expr. Это означает, что порядок определений в объявлении opt-decl-string несущественен.

Контекстные условия. Входящие в локальное выражение объявления decl должны быть совместимы.

Максимальный тип выражения value_expr не должен включать в себя абстрактные типы, переменные и каналы, определенные в объявлениях decl.

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

Локальное выражение local_expr статически производит доступ к тем нелокальным переменным и каналам (т.е. к переменным и каналам, не определяемым в объявлении opt-decl-string), к которым статически обращается входящее в его состав выражение value_expr.

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

В конце вычисления выражения value_expr любое ожидающее обработки взаимодействие по каналу, объявленному в объявлении opt-decl-string, замещается на stop.

6.23.2. Let-выражения (Let Expressions)

Синтаксис.

let_expr ::=

let let_def-list in value_expr end

let_def ::=

typing ½

explicit_let ½

implicit_let

explicit_let ::=

let_binding = value_expr

implicit_let ::=

single_typing restriction

let_binding ::=

binding ½

record_pattern ½

list_pattern

Контекстно-независимые расширения. Выражение let_expr, содержащее в себе более одного определения let_def, является сокращенной формой записи для некоторого числа вложенных let-выражений с единственным определением. То есть выражение let_expr вида:

let let_def1, …, let_defn in value_expr end

является сокращенной формой записи следующего выражения:

let let_def1 in

let let_defn in value_expr end

end

Контекст и правила видимости. В выражении let_expr вида:

let let_def in value_expr end

контекстом определения let_def является выражение value_expr.

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

В явном определении explicit_let максимальным контекстным типом конструкции let_binding является максимальный тип выражения value_expr.

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

Указание типа typing не обращается статически ни к каким переменным или каналам.

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

Неявное определение implicit_let статически производит доступ к тем переменным и каналам, к которым статически обращается входящее в его состав ограничение restriction.

Семантика. Выражение let_expr, содержащее одно определение let_def и имеющее вид:

let let_def in value_expr end

вычисляется следующим образом. Определение let_def представляет некоторое множество моделей, как описано ниже. Указанное выражение value_expr вычисляется в каждой такой модели и между результирующими эффектами этих вычислений производится недетерминированный выбор.

Различаются три вида определений let_def:

  • определение let_def в форме указания типа typing представляет множество моделей, которые удовлетворяют определениям, заданных указанием типа typing;

  • определение let_def в неявной форме implicit_let представляет некоторое подмножество моделей, которые удовлетворяют определениям, заданных указанием типа single_typing: тех из них, где выполняется ограничение restriction;

  • определение let_def в явной форме explicit_let представляет множество моделей, получаемое следующим образом. Выражение value_expr вычисляется, и затем возвращаемое им значение сопоставляется со связыванием let_binding. Если данное значение соответствует связыванию let_binding, результатом является некоторый набор определений и искомое множество моделей содержит единственную модель, удовлетворяющую этим определениям. Если же, напротив, данное значение не соответствует связыванию let_binding, то искомое множество моделей пусто.

6.23.3. If- выражения (If Expressions)

Синтаксис.

if_expr ::=

if logical-value_expr then

value_expr

opt-elsif_branch-string

opt-else_branch

end

elsif_branch ::=

elsif logical-value_expr then value_expr

else_branch ::=

else value_expr

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

if value_expr1 then value_expr1

elsif value_expr2 then value_expr2¢

elsif value_exprn then value_exprn¢

opt-else_branch

end

является сокращенной формой записи выражения:

if value_expr1 then value_expr1else

if value_expr2 then value_expr2¢ else

if value_exprn then value_exprn¢ opt-else_branch end

end

end

Выражение if_expr вида:

if value_expr1 then value_expr2 end

является краткой записью выражения:

if value_expr1 then value_expr2 else skip end

Контекстные условия. В выражении if_expr вида:

if value_expr1 then value_expr2 else value_expr3 end

максимальным типом выражения value_expr1 должен быть тип Bool и максимальные типы выражений value_expr2 и value_expr3 должны иметь наименьшую верхнюю границу.

Атрибуты. Для if-выражения вида:

if value_expr1 then value_expr2 else value_expr3 end

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

Рассматриваемое выражение if_expr статически обращается к тем переменным и каналам, к которым статически обращаются выражения value_expr1, value_expr2 и value_expr3.

Семантика. Результирующее воздействие выражения if_expr состоит в том, чтобы определить применимую альтернативу и получить эффект от ее применения. Выражение if_expr вида:

if value_expr1 then value_expr2 else value_expr3 end

вычисляется путем вычисления выражения value_expr1, которое возвращает некоторое булевское значение — тестовое значение. Если полученное тестовое значение равно true, вычисляется выражение value_expr2. В противном случае (значение тестового выражения равно false) вычисляется выражение value_expr3.

6.23.4. Case-выражения (Case Expressions)

Синтаксис.

case_expr ::=

case value_expr of case_branch-list end

case_branch ::=

pattern value_expr

Контекст и правила видимости. В ветви case_branch контекстом образца pattern является выражение value_expr.

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

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

В выражении case_expr максимальным контекстным типом образцов pattern в ветвях case_branch является максимальный тип выражения value_expr.

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

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

Семантика. Результирующее воздействие выражения case_expr состоит в том, чтобы вычислить выражение value_expr, определить соответствующую ветвь case_branch и затем вычислить выражение value_expr, содержащееся в этой ветви. Выражение value_expr вычисляется и возвращает некоторое значение — тестовое значение. Затем просматриваются слева направо ветви case_branch до тех пор, пока данное тестовое значение не совпадет с каким-либо образцом pattern. Такое успешное сопоставление образца с тестовым значением дает в результате некоторый набор определений. В завершении в контексте этих определений вычисляется соответствующее выражение value_expr, содержащееся в ветви case_branch, на которой произошло отождествление образца и тестового значения.

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

Тип файла
Документ
Размер
776,5 Kb
Тип материала
Высшее учебное заведение

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

Свежие статьи
Популярно сейчас
Как Вы думаете, сколько людей до Вас делали точно такое же задание? 99% студентов выполняют точно такие же задания, как и их предшественники год назад. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6510
Авторов
на СтудИзбе
302
Средний доход
с одного платного файла
Обучение Подробнее