методичка (811291), страница 10

Файл №811291 методичка (Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL) 10 страницаметодичка (811291) страница 102020-08-21СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

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

Рассмотрим несколько примеров в области видимости объявлений:

value e, e1, e2 : T

channel c , c1, c2: T

variable x : T

Отличие взаимной блокировки от параллельной композиции иллюстрируют две следующие эквивалентности:

x := c? ++ c!e is x := e

x := c? || c!e is (x := e) |^| ((x := c?; c!e)|=|(c!e; x := c?)|=|(x := e))

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

Взаимная блокировка наглядно иллюстрирует также различие между внешним и внутренним выбором:

(x := c1? |=| c2!e2) ++ c1!e1 is x := e1

(x := c1? |^| c2!e2) ++ c1!e1 is x := e1 |^| stop

При внутреннем выборе может произойти останов из-за невозможности выполнить взаимодействие (c2!e2 ++ c1!e1). Такая тупиковая ситуация специфицируется в RSL предопределенным выражением stop.

Другим примером того, как невозможность взаимодействия с окружением приводит к останову, является эквивалентность:

x := c1? ++ c2!e is stop

Для параллельной композиции соответствующая эквивалентность принимает вид:

x := c1? || c2!e is (x := c1?; c2!e) |=| (c2!e; x := c1?)

и выражает тот факт, что поскольку данные выражения не могут взаимодействовать друг с другом, для них возможно только взаимодействие с окружением.

Упрощение параллельных выражений

При упрощении параллельных выражений кроме указанных свойств полезно иметь в виду следующие эквивалентности:

value_expr1 || (value_expr2 |^| value_expr3) is

(value_expr1 || value_expr2) |^| (value_expr1 || value_expr3)

value_expr1 ++ (value_expr2 |^| value_expr3) is

(value_expr1 ++ value_expr2) |^| (value_expr1 ++ value_expr3)

Кроме того, если выражения value_expr, value_expr1 и value_expr2 не вызывают взаимодействия и c1 ~= c2, то справедливы свойства:

x := c1? || c2! value_expr is (x := c1?; c2! value_expr) |=| (c2! value_expr; x := c1?)

x := c? || c! value_expr is (x := value_expr) |^|

((x := c?; c! value_expr)|=|(c! value_expr; x := c?)|=|(x := value_expr))

x := c1? ++ c2! value_expr is stop

x := c? ++ c! value_expr is x := value_expr

(x := c1? |=| c2! value_expr2) ++ c1! value_expr1 is x := value_expr1

(x := c1? |^| c2! value_expr2) ++ c1! value_expr1 is (x := value_expr1) |^| stop

Упражнения

Упростить следующие параллельные выражения в предположении, что произошли все возможные взаимодействия:

  1. (b!2) || (y := a?) || if (x := 1); (a!x); (true |^| false) then a!(b?) else a!(1 + b?) end

  1. (b!2) || (x := a?) || if (a!3; true) |^| ((a!b? + 5); false) then a!(b?)

else a!(1 + b?) end || (a!0)

  1. (if (a?) > 0 then b!1 else b!2 end ++( a!1; x := b?; b!4)) ||

(y := if (b?) = 1 then a? else (0 - a?) end) || (a!0)

  1. a!(5 + b?) || ((x := (if true |^| false then x := b?; 1 else b!3; x := 2; 6 end) + x) ++

(b!4 || y := b?))

  1. a!(5 + a?) || ((x := (if true |^| false then x := b?; 1 else x := b?; 6 end)) ++

(b!4 || x := a? || a!3 || y := b?))

  1. case (1 |^| b?) of

1 -> x := a? + 1,

2 -> x := b?,

3 -> y := a? + 3,

4 -> y := b? + a?,

5 -> x := y := a?; y

end || a!1 || b!(a? + 2) || a!3

  1. case (1 |^| b?) of

1 -> x := a? + 1,

2 -> x := b? |^| a?,

3 -> y := a? + 3,

4 -> y := b? + a?,

5 -> x := y: = a?; y

end || a!0 || b!(a? + a?) || a!2 || a!3

  1. case (a?) of

0, 1 -> x := a? + 1,

2 -> x := b?,

3 -> y := a? + 3,

4 -> y := b? + a?

end || (x := a?; a!0 |=| b!(a?)) || a!4

ГЛАВА 10. Недетерминизм и неполные спецификации

Понятие недетерминизма и неполной спецификации. Источники недетерминизма в спецификациях. Недетерминизм в case- и let-выражениях. Упражнения.

Понятие недетерминизма и неполной спецификации

Понятия недетерминизма и неполной спецификации имеют разную природу, но, вместе с тем, в спецификациях часто встречаются в похожих ситуациях, поэтому имеет смысл рассмотреть эти понятия совместно.

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

  • ДсДм - детерминированная система и детерминированная модель - это простейший случай;

  • НсДм - недетерминированная система и детерминированная модель

  • НсНм - недетерминированная система и недетерминированная модель

  • ДсНм - детерминированная система и недетерминированная модель.

Пропуская случай ДсДм как достаточно простой, начнем сразу со второго случая. Вариант НсДм используется тогда, когда модель существенно упрощает поведение реальной системы и вместо рассмотрения разнообразных результатов/поведений, которые можно ожидать от реальной системы рассматривается один из возможных вариантов. Такие модели часто используются при прототипировании, когда важно сосредоточиться на одних вопросах функциональности и архитектуры и можно временно отвлечься от других. Заметим, для целей верификации такое соотношение системы модели может породить ряд трудностей, так, например, система, будучи недетерминированной, будет демонстрировать поведение, не предусмотренное моделью.

Необходимость случая НсНм также достаточно понятна - для системы со сложным, недетерминированным поведением приходится вводить в рассмотрение недетерминированную модель. При этом нужно иметь в виду, что наблюдаемое поведение системы и модели могут существенно различаться. В частности, на некоторых отрезках времени система может вести себя детерминировано, модель - недетерминировано, и - наоборот. Таким образом, соответствие поведений системы и модели в данном случае вопрос не простой.

Последний случай ДсНм кажется надуманным - не понятно, для чего моделировать детерминированную систему при помощи недетерминированной модели, то есть с поведением более разнообразным, чем поведение реализации. Но примеры такого сочетания тоже могут встретиться. Так рассмотрим систему, которая обрабатывает некоторые данные высокоточного вычислителя и выдает округленный результат. В требованиях к системе написано, что округление можно проводить любым из способов, который реализован в использованном аппаратном процессоре, и это требование должно быть формализовано в спецификациях. Большинство процессоров реализуют либо округление к ближайшему целому, либо выполняют отбрасывание дробной части. В этих предположениях системы, которые будут выдавать в качестве результата ближайшее приближение исходных данных, не превышающее его, или не превосходящие его, или случайным образом выбирающие приближение сверху или снизу – все они отвечают требованиям модели. Пусть в спецификации не задается, каким именно образом выполняется округление и, если результат подходит под один из вариантов, описанных выше, он считается правильным. Тогда получается, что модель является недетерминированной, а в трех рассмотренных случаях только в последнем реализация недетерминирована, в первых двух она вполне детерминирована.

Неполная спецификация или недоспецификация, естественно может возникнуть на практике как результат ошибки ее разработчика или как результат его недобросовестного отношения к работе. Мы рассматриваем другую ситуацию, когда спецификация должна быть неполной. В каких случаях это бывает на практике? Имеется две основные причины, обуславливающих необходимость недоспецификации. Во-первых, это стремление к повышению уровня абстракции и нарочитом игнорировании деталей, чтобы дать разработчику реализации более широкое поле для поиска наилучших с его точки зрения решений. Во-вторых, причиной может быть отсутствие некоторых знаний в момент разработки спецификаций.

Пример. На ранней фазе проектирования уже принято решение, что размер пакетов данных будет ограничен некоторой константой, но величина этой константы еще не выбрана. Это дает основание ввести такую константу (имя константы) в формальную спецификацию, что, в частности, позволит вполне формально описывать некоторые свойства системы (например, длина элемента пакета не должна превышать максимальную длину пакета). Собственно ограничение на размер будет сформулировано в реализации. Заметим, что различные реализации при этом могут иметь различные ограничения на размер, но многие их свойства будут сформулированы в спецификациях в общем виде, не зависящем от деталей реализации.

Иногда недоспецификация и недетерминизм в формальном тексте на RSL выглядят очень похоже. Покажем на типовых примерах, что мы будем называть недоспецификацией и что – недетерминизмом.

Рассмотрим примеры определения недоспецифицированных констант и функций:

value x : Int,

y : Int :- y ~= 0

axiom y ~= 3

Константа x может иметь любое целое значение. Константа y может иметь любое целое значение за исключением 0 и 3.

value f : Int -> Int

axiom forall x : Int :- f(x) > x

Функция f выдает результат, превосходящий значение аргумента.

Заметим, что f описана как детерминированная функция. Это значит, что в ответ на вызов с одним и тем же аргументом она должна отвечать всегда одним и тем же результатом, конкретное значение которого пока не специфицировано.

Вот примеры недетерминированных функций:

value f : Int -~-> Int

axiom forall x : Int :-

(f(x) = x-1) \/

(f(x) = x) \/

(f(x) = x+1)

Функция f возвращает как результат целое значение, которое отличается от аргумента не более, чем на единицу.

Функция недетерминирована, то есть при вызове с одним и тем же аргументом будет давать, возможно, разные результаты.

value f : Int -~-> Int

f(x) is let y : Nat :- x-1 <= y /\

y <= x+1

in y end

Это полностью эквивалентное определение функции f.

value f : Int -~-> Int

f(x) is x-1 |^| x |^| x+1

Еще одно эквивалентное определение функции f, которое использует комбинатор внутренний выбор.

Заметим, что при использовании имплицитного (неявного) определения при помощи пост-условия функция определяется как детерминированная. Так, очень близкое по смыслу определение функции f1 будет определением детерминированной функции (при этом можно считать функцию недоспецифицированной):

value f1 : Int -> Int

f1(x) as r

post (r <= x+1) /\ (r >= x-1)

Источники недетерминизма в спецификациях

В какой форме недетерминизм может появиться в спецификациях? Перечислим основные возможности:

  • выражения с использованием комбинатора внутренний выбор

  • let-выражения в неявной форме

  • особые случаи использования case- и let-выражения с record pattern

  • выражения, использующие комбинатор внешний выбор и параллельные вычисления, вообще.

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

Рассмотрим часто встречающиеся ошибки при использовании недетерминированных спецификаций. Первая из них – чисто техническая, забывают, что недетерминированная функция не может быть всюду вычислимой (total):

value f : Int -> Int f(x) is 0 |^| 1 |^| 2

Правильно писать:

value f : Int -~-> Int f(x) is 0 |^| 1 |^| 2

Вторая ошибка – попытка определения «недетерминированной константы», например:

value x : Int = 0 |^| 1 |^| 2

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

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

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