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

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

Текущая версия

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

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

value
  MAX_PACKET : Int

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

value
  MAX_PACKET : Int := MAX_PACKET ≥ 1024

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

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

channel
  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.