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

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

Версия от 03:50, 25 сентября 2008; ESyr01 (Обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

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

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

Н. с. --- с., пис. не все детали реализации

'''value'''
   MAX_PACKET : Int

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

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

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

Летор просит завписать в тетр. опр. 4 понятий: 
# Неп. спец. конст
# Неп. спец. функции
# Недетерм. спец. конст.
# Недетерм. спец. функции

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

В 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, для них не опр. присв, но есть тип:

'''channe'''
   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.name/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