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

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

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

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

Контекстные условия. В аппликативном выражении application_expr, имеющем только один фактический параметр actual_function_parameter, максимальный тип выражения value_expr должен быть либо списком, либо отображением, либо функциональным типом. Кроме того, если максимальный тип выражения value_expr является:

  • типом список — tw, то максимальным типом фактического параметра actual_function_parameter должен быть Int;

  • типом отображение — t1 t2, то максимальный тип фактического параметра actual_function_parameter должен быть меньше или равен типу t1;

  • функциональным типом — t1 oads t2, то максимальный тип фактического параметра actual_function_parameter должен быть меньше или равен типу t1.

Атрибуты. Максимальный тип аппликативного выражения application_expr, имеющего только один фактический параметр actual_function_parameter, определяется максимальным типом входящего в его состав выражения value_expr. А именно, если максимальный тип данного выражения value_expr является:

  • типом список — tw, то максимальный тип аппликативного выражения application_expr представляет собой тип t элементов этого списка;

  • типом отображение — t1 t2, то максимальный тип аппликативного выражения application_expr представляет собой тип t2 области значения этого отображения;

  • функциональным типом — t1 oads t2, то максимальный тип аппликативного выражения application_expr представляет собой тип результата t2.

Максимальным типом фактического параметра actual_function_parameter, имеющего в своем составе одно выражение value_expr, является максимальный тип этого выражения value_expr. Фактический параметр actual_function_parameter указанного вида статически производит доступ к тем переменным и каналам, к которым статически обращается выражение value_expr.

Аппликативное выражение application_expr, имеющее только один фактический параметр actual_function_parameter, статически производит доступ к тем переменным и каналам, к которым статически обращаются входящие в его состав выражение value_expr и фактический параметр actual_function_parameter. Кроме того, если максимальным типом указанного выражения value_expr является функциональный тип t1 oads t2, то аппликативное выражение application_expr статически производит доступ также и к тем переменным и каналам, к которым статически обращается тело функции согласно описанию доступа oads.

Семантика. Результирующее воздействие аппликативного выражения application_expr заключается в применении некоторого значения, представляющего собой список, отображение или функцию, к какому-либо фактическому параметру.

Результирующее воздействие аппликативного выражения application_expr вида value_expr1( value_expr2 ) состоит в вычислении выражения value_expr2 для получения фактического параметра, затем вычислении значения выражения value_expr1 и, наконец, применении полученного значения к указанному фактическому параметру. При этом в зависимости от вида значения, которое применяется к фактическому параметру, такое применение выполняется следующим образом:

  • если данное значение представляет собой список, то фактический параметр должен принадлежать множеству индексов данного списка (множеству целых чисел в диапазоне от 1 до длины списка). В этом случае возвращаемым значением становится элемент списка, стоящий в данной позиции. В противном случае результат применения является недоспецифицированным.

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

  • если данное значение является функцией, то соответствующая функция применяется к указанному фактическому параметру.

6.11. Квантифицированные выражения (Quantified Expressions)

Синтаксис.

quantified_expr ::=

quantifier typing-list restriction

quantifier ::=

 ½

 ½



Контекст и правила видимости. В квантифицированном выражении quantified_expr контекстом входящих в него конструкций typing является ограничение restriction.

Атрибуты. Максимальным типом квантифицированного выражения quantified_expr является Bool.

Квантифицированное выражение quantified_expr статически производит доступ к тем переменным и каналам, к которым статически обращается входящее в его состав ограничение restriction.

Семантика. Результирующее воздействие квантифицированного выражения 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_condition

pre_condition ::=

pre readonly_logical-value_expr

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

Выражение value_expr, входящее в состав предусловия pre_condition, должно представлять собой read-only выражение и его максимальный тип должен быть Bool.

Контекстно-зависимые расширения. Выражение эквивалентности equivalence_expr вида:

value_expr1 value_expr2 pre value_expr3

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

( value_expr3true )  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_condition

post_condition ::=

opt-result_naming post readonly_logical-value_expr

result_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_expr2true )  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_expr2

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

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

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

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