Редактирование: МФСП, 04 лекция (от 24 сентября)

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

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

Неполная спецификация.

Неполная спецификация --- спецификация, описывающая не все детали реализации

'''value'''
   MAX_PACKET : Int

Мы можем указать границы, в которых находится константа, но эта спецификация также будет неполна:

'''value'''
   MAX_PACKET : Int := MAX_PACKET &ge; 1024

Недетерминированная функция — функция, которая при одном и том же значении возвращает различные результаты.

# Неполная спецификация констант — когда недостаточно информации для получения значения константы
# Неполная спецификация функции — когда недостаточно информации для получения значения функции
# Недетерминированная спецификация константы — когда константа определена так, что её значение неизвестно
# Недетерминированная спецификация функции — когда функция определена так, что её значение для пр. набора (наборов) параметров неизвестно

В RSL нет возможности представить недетерминизм констант, и там такого понятия нет.

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

И ситуация, когда мы не написали ничего, кроме сигнатуры — типичный пример неполной спецификации. Или же мы написали только постусловие или аксиому, неполное описание поведение функции. Например:

'''value'''
   f : Int &rarr; Int
     f(x) '''as''' y
       '''post''' (y=) &or; (y=x-1) &or; (y=x+1)

Насколько мы могли знать из семинаров, бывают полностью пр. и неполно определённые функции. Неполно определённые обозначаются в ASCII-нотации как ~&rarr;. При исп. &rarr; известно, что функция является детерминированной и тотальной. При использовании ~&rarr; функция может быть нетот. и недетерминированной.

Если же функция может детерминированно менять значение, то мы сможем описать некое условие на некое дополнительное множество, которое введём специально. И можно ввести дополнительные условия, чтобы но удовлетворяющие некоему распределению с произвольной точностью. обычно это актуально при введении функции генерации сл. значений.

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

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

1.
 '''value'''
   MAX_PACKET : Int
2.
 '''value'''
   f : Int &rarr; Int
4.
 '''value'''
   f : Int ~&rarr; Int
     f(x) as y
       '''post''' (y > 0)

Единственное отличие — какой синтаксис использовать — написать аксиому, или ещё что. Второй вариант — константный предметной области, диапазон, список (коды ошибок).

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

Что касается вопроса относительно спецификации алгоритма, то в RSL, когда мы описываем спецификацию, мы описываем её значимое и побочное действие. Ограничения на внутреннюю реализацию на RSL никак описаны быть не могут, кроме как придумывая синтетический способ.

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

Пример недоспецификации и неполной спецификации — когда задан RNG, у которого не задано распределение.

Рассмотрим соотношение между моделью и системой, реализация, которая специфицируется. Есть модель, есть реализация, система, её реализующая. Может быть 4 вариант, когда модель является детерминированной и система детерминирована, модель недетерминирована и система детерминирована, модель детерминирована, система недетерминирована, и когда обе системы недетерминированы.

С первым случаем всё достаточно понятно. Второй вариант, когда модель является недетерминированной, а система, её реализация, является детерминированной, достаточно странный вариант, но в природе существовать может. Например, стандарт POSIX. Если стандарт не требует конкретного значения, описания кода ошибки, а система при этом конкретные значения приписывает. Этот пример неправильный, поскольку в этом случае модель неполна. Это действительно странный случай, когда мы описываем, что функция может возвращать недетерминированное значение, а реализация при этом детерминирована. Здесь говорится о недетерминированности с т.з. спецификации. Например, если реализация имеет внутренний счётчик и каждый раз, инкримирует его, возвращает значение, то этот недетерминизм пр. с т.з. специф. f : Int ~&rarr; Int f(x) as y '''post''' (y > 0).

Как мы выяснили, понятие детерминизма-недетерминизма реализации рассматривается тн. модели, а не по своим внутренним зар-кам.

Какие ещё пример: мель детали, системы недетерминированы. Это достаточно реальный пример, может встретиться, когда спецификация неполна. Например, если в спецификации результирующего типа  Bool, а в реализации — Int, и в качестве True возвращается значение, отл. от 0. При этом это некий мухлёж, это недетерминизм уже внутри реализации.

Описание типа множество:
 '''type'''
   Set == empty | add(Elem, Set)
 '''axiom'''
   &forall; e, e1, e2 : Elem, s : Set :-
     [no_duplicates]
       add(e, add(e,s)) is add(e, s)
     [unordered]
       add(e1, add(e2, s)) is add(e2, add(e1, s))

Каким образом может появиться недетерминизм? Можно легко написать такую реализацию:

case s of
   add(x,y) &rarr; x
 end

В RSL можно писать по таким определениям case, когда мы выбираем по некоторому множеству, мы пишем некоторый паттерн по операции из вариант. пр. этого типа с двумя параметрами, и подразумеваем, что это может быть любое ..., сзд. множеств, а поскольку есть аксиома неуп., то в качестве x и y подбирается заранее неизвестно какая пара, поэтому это выражение будет недетерминировано. Можно написать ещё кое-что в нед.:

let x : Int in x end

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

В языке RSL есть такое понятие как канал. Они имеют синтаксис такой же, как и у переменных, только вместо value пишется channel, для них не определено присваивание, но есть тип:

'''channel'''
   c1:int, c2 : Char

Если у каналов разные идентификаторы, то они разные и равными оказаться не могут.

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

'''value'''
   f : Unit -~&rarr; Int in c1 out c2

при этом функция читает из c1 и пишет в c2 в данном случае.

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

'''value''' f(x) is
   y := c1? #считывание из канала. Тип выр. совп. с типом канала.
   с2!expr № Запись в канал. Тип выр. должен совп. с типом канала.

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

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

Первый, простой способ — параллельная композиция: f1 || f2. Это означает, что они работают параллельно и могут взаимодействовать по общему каналу. А могут и не взаимодействовать. 
 c!5 || x := c?
Это может произойти, а может и нет. Это не эквивалентно присваиванию 5 в x.

с!& || (x :=c? || c!5)
может быть эквивалентно:
 x:=5; c!7
 x:=7; c!5
или как-то иначе.

Второй вариант композиции: внешний выбор. |=| Он говорит то, что как поведёт себя система, зависит от внешнего окружения.

x := c? |=| d!5
То, как поведёт себя система, зависит от внешнего окруженияя 
 (x := c? |=| d!5) || c!1
Это будет экв. 
 x:=1

|^| — внутренний выбор. Это говорит, что выбор происходит не от окр., а по внутренним сображениям процесса.
 (x := c? |^| d!5) || c!1
Результат в этом случае вполне мог быть либо
 (c:=c?||c!1)
либо
 (d!5||c!1)
Это отличие внутреннего выбора от внешнего.

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

4 вариант композиции — взаимная блокировка, обозначается ++. Все взаимодействующие должны пройти между выр., композирующих с помощью взаимной блокировки.
 (x:=c?++c!e) == (x:=e)
Если для параллельной композиции взаимодействие необязательно, то в случае блокировки взаимодействие обязательно.
 (x:=c?||c!e) == (x:=e) |^| ((x:=c?; c!e) |=| (c!e; x:=c?) |=| (x:=e))

Все взаимодействия происходят синхронно.

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

Пример на interlock, иллюстрирует отличие между внешним и внутренним выбором:
//Все каналы блокируются, небуферизованные.

((x:=c1?|=|c2!e2)++c1!e1) == x:=e
 ((x:=c1?|^|c2!e2)++c1!e1) == x:=e |^| stop #stop — специфическое ключевое слово в RSL, обозначает блокировку, тупиковую ситуацию, когда вычисление дальше идти не может.

Как ещё появляется недетерминизм в RSL? Оператор недетерминированного внутреннего выбора — оператор, привносящий недетерминизм в язык. Можно написать 1|^|2 — явное выражение, являющееся недетерминированным.

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

Некие эквивалентности, полезные для упрощения выражений, это в методичке есть:
 expr1||(expr2|^|expr3) is (expr1||expr2)|^|(expr1||expr3)
 expr1++(expr2|^|expr3) is (expr1++expr2)|^|(expr1++expr3)
Если у нас каналы… в предположении, что expr1 и expr2 не взаимодействуют, то справедливо след. свойство:
 x:=c1?||c2!expr == (x:=c1;c2!expr)|=|(c2:=expr; x:=c1?)

//== и is — граф. и ASCII-нотация

x:=c? || c!expr == x:=expr |^| ((x:c?;c!expr)|=|(c!expr;x:=c)|=|(x:=expr))

На экзамене будут задачи на упрощение параллельных выражений, где будут встречаться все виды из этих 4 композиций, и внутри отдельных подпроцессов могут встретиться if, недетерминированные выборы или же case.

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_04_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_24_%D1%81%D0%B5%D0%BD%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29

@@ Строка 175: / Строка 175: @@
 На экзамене будут задачи на упрощение параллельных выражений, где будут встречаться все виды из этих 4 композиций, и внутри отдельных подпроцессов могут встретиться if, недетерминированные выборы или же case.
-{{МФСП}}
+{{МСФП}}
 {{Lection-stub}}

Редактирование: МФСП, 04 лекция (от 24 сентября)

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты