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

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

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

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

value
  MAX_PACKET : Int

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

value
  MAX_PACKET : Int := MAX_PACKET ≥ 1024

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

Лектор просит записать определения 4 понятий:

1. Неполная спецификация констант
2. Неполная спецификация функции
3. Недетерминированная спецификация констант
4. Недетерминированная спецификация функции

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

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

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

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

value
  f : Int → Int
    f(x) as y
      post (y=) ∨ (y=x-1) ∨ (y=x+1)

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

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

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

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

1.

value
  MAX_PACKET : Int

2.

value
  f : Int → Int

4.

value
  f : Int ~→ Int
    f(x) as y
      post (y > 0)

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

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

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

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

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

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

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

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

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

Описание типа множество:

type
  Set == empty | add(Elem, Set)
axiom
  ∀ 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) → x
end

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

let x : Int in x end

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

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

channe
  c1:int, c2 : Char

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

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

value
  f : Unit -~→ 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.