Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 11

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

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

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

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

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

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

Покажем на типовых примерах, что мы будем называтьнедоспецификацией и что – недетерминизмом.Рассмотрим примеры определения недоспецифицированных констант ифункций:value x : Int,y : Int :- y ~= 0axiom y ~= 3Константа x может иметь любое целоезначение. Константа y может иметьлюбоецелоезначениезаисключением 0 и 3.59value f : Int -> Intaxiom forall x : Int :- f(x) > xФункцияfвыдаетрезультат,превосходящий значение аргумента.Заметим,чтоfописанакакдетерминированнаяфункция.Этозначит, что в ответ на вызов с одним итем же аргументом она должнаотвечать всегда одним и тем жерезультатом, конкретное значениекоторого пока не специфицировано.Вот примеры недетерминированных функций:value f : Int -~-> Intaxiom forall x : Int :(f(x) = x-1) \/(f(x) = x) \/(f(x) = x+1)Функция f возвращает как результатцелое значение, которое отличается отаргумента не более, чем на единицу.Функция недетерминирована, то естьпри вызове с одним и тем жеаргументом будет давать, возможно,разные результаты.value f : Int -~-> Intf(x) is let y : Nat :- x-1 <= y /\y <= x+1in y endЭтополностьюопределение функции f.value f : Int -~-> Intf(x) is x-1 |^| x |^| x+1Еще одно эквивалентное определениефункцииf,котороеиспользуеткомбинатор внутренний выбор.эквивалентноеЗаметим, что при использовании имплицитного (неявного) определения припомощи пост-условия функция определяется как детерминированная.

Так, оченьблизкое по смыслу определение функции f1 будет определениемдетерминированнойфункции(приэтомможносчитатьфункциюнедоспецифицированной):valuef1 : Int -> Intf1(x) as rpost (r <= x+1) /\ (r >= x-1)Источники недетерминизма в спецификацияхВ какой форме недетерминизм может появиться в спецификациях?Перечислим основные возможности:• выражения с использованием комбинатора внутренний выбор• let-выражения в неявной форме• особые случаи использования case- и let-выражения с record pattern• выражения, использующие комбинатор внешний выбор и параллельныевычисления, вообще.60Кроме того, часто (но не всегда), если в выражении используется обращение кнедетерминированнойфункции,тоисамовыражениестановитсянедетерминированным.Рассмотримчастовстречающиесяошибкиприиспользованиинедетерминированных спецификаций.

Первая из них – чисто техническая,забывают, что недетерминированная функция не может быть всюду вычислимой(total):value f : Int -> Intf(x) is 0 |^| 1 |^| 2Правильно писать:value f : Int -~-> Intf(x) is 0 |^| 1 |^| 2Вторая ошибка – попытка определения «недетерминированной константы»,например:value x : Int = 0 |^| 1 |^| 2Value-expression в определениях констант и все предикаты в RSL – этодетерминированные выражения.Еще один важный случай, когда недетерминизм фактически запрещен – этопредикаты, использующиеся как описания ограничений в аксиомах, пред- и постусловиях, в других описаниях. Недетерминированный предикат тождественен false.Так, выражение:axiom let b : Bool in b endтождественно равно false, так как предикат, стоящий после слова axiom являетсянедетерминированным. Следующий пример:exists x : Char :- let y : Char in y endЭто выражение также равно false, так какнедетерминирован.

Следовательно, выражение:ограничивающийпредикат{ x | exists x : Char :- let y : Char in y end }описывает пустое множество. Такие же правила использования предикатовсправедливы в сокращенных описаниях списков и отображений, в описанияхподтипов и в имплицитной форме let-выражения.Недетерминизм в case- и let-выраженияхИз перечисленных выше источников недетерминизма отдельного вниманиязаслуживает недетерминизм в case- и let-выражениях. Рассмотрим следующееопределение множества, которое строится при помощи конструкторов empty и add:typeSet == empty | add(Elem, Set)axiom forall e, e1, e2 : Elem, s : Set :[no_duplicates]add(e, add(e,s)) is add(e,s)[unordered]61add(e1, add(e2,s)) is add(e2, add(e1,s))Попробуем написать выражение, которое будет выбирать из значения типаSet некоторый (произвольный) элемент множества. В предположении, чтоx – это переменная типа Set иx ≠emptyтаким выражением может быть либоlet add(x, y) = s in x endлибоcase s ofadd(x, y) -> xendОба вышеприведенных выражения являются в общем случаенедетерминированными, так как при данном определении Set , например, верно,что, если s= add(a, add(b, empty), то в силу аксиомы [unordered], верно, что s= add(b,add(a, empty ).

Следовательно, и в случае let, и case значение этих выражений можетравняться либо a, либо b, то есть выражения – недетерминированы.Упражнения1. Описать недетерминированную функцию, которая выбирает из множестванекоторый элемент.2. Описать детерминированную функцию, которая выбирает из множестванекоторый элемент. (При необходимости введите дополнительные ограниченияна тип элементов).3.

Привести пример, когда комбинация двух недетерминированных функций даетдетерминированный результат.4. Какое из приведенных ниже выражений является недетерминированным?(a!1) || (b!1) || (x:=a?) || (x:=b?)((a!1) || (b!1)) |=| ((x:=a?) || (x:=b?))(a!1) || (b!1) || ((x:=a?) |=| (x:=b?))5. Привести пример case- и let-выражений, которые дают недетерминированныйрезультат. Перепишите спецификацию таким образом, чтобы все возможныеповедения были представлены в форме детерминированных выражений,объединенных комбинатором |^|.62ГЛАВА 11.

ЗАДАНИЕ ПРАКТИКУМАПостановка задачи. Варианты заданий. Требования и методические указания длявыполнения задания.Постановка задачиРазработать на языке RSL спецификацию программного интерфейсаопределяемой вариантом задания системы в виде:- явной моделе-ориентированной спецификации,- неявной моделе-ориентированной спецификации,- алгебраической спецификации.При описании интерфейса предложенной системы предусмотреть в егосоставе операции по формированию информационной базы системы,обеспечивающей возможность накапливать и использовать необходимуюинформацию. Способ представления такой информационной базы выбратьсамостоятельно. В предложенных ниже вариантах заданий дается лишь краткоеописание программных систем с указанием минимально необходимого набораопераций, тем самым разработчику спецификаций предоставляется возможностьрасширить этот набор по своему усмотрению.Варианты заданий1.

Система учета ″автомобили – владельцы – доверенности″.Система должна обеспечивать следующие возможности: добавлять/удалятьнового владельца и соответственно новый автомобиль для заданного владельца,осуществлять аналогичные операции с доверенностями на автомобиль,выдавать необходимую справочную информацию (например, для указанногоавтомобиля определять его владельца и т.д.), при этом предполагается, что укаждого автомобиля может быть только один владелец, на один и тот жеавтомобиль может быть зафиксировано несколько доверенностей.2. Генеалогическое дерево.Система поддержки генеалогического дерева должна предоставлять следующиевозможности: добавлять в дерево нового члена семьи (ребенка, супруга,предка), вносить изменения в узлы дерева (например, фиксировать сменуфамилии или дату смерти), осуществлять поиск полезной информации подереву (например, для указанного члена семьи находить его детей и наоборот).3.