Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 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_expr₁ || (value_expr₂ |^| value_expr₃) is

(value_expr₁ || value_expr₂) |^| (value_expr₁ || value_expr₃)

value_expr₁ ++ (value_expr₂ |^| value_expr₃) is

(value_expr₁ ++ value_expr₂) |^| (value_expr₁ ++ value_expr₃)

Кроме того, если выражения value_expr, value_expr₁ и value_expr₂ не вызывают взаимодействия и 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_expr₂) ++ c1! value_expr₁ is x := value_expr₁

(x := c1? |^| c2! value_expr₂) ++ c1! value_expr₁ is (x := value_expr₁) |^| 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 выглядят очень похоже. Покажем на типовых примерах, что мы будем называть недоспецификацией и что – недетерминизмом.

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

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

Заметим, что при использовании имплицитного (неявного) определения при помощи пост-условия функция определяется как детерминированная. Так, очень близкое по смыслу определение функции 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

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

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