МФСП, 04 лекция (от 24 сентября)
Материал из eSyr's wiki.
Неполная спецификация.
Неполная спецификация --- спецификация, описывающая не все детали реализации
value MAX_PACKET : Int
Мы можем указать границы, в которых находится константа, но эта спецификация также будет неполна:
value MAX_PACKET : Int := MAX_PACKET ≥ 1024
Недетерминированная функция — функция, которая при одном и том же значении возвращает различные результаты.
- Неполная спецификация констант — когда недостаточно информации для получения значения константы
- Неполная спецификация функции — когда недостаточно информации для получения значения функции
- Недетерминированная спецификация константы — когда константа определена так, что её значение неизвестно
- Недетерминированная спецификация функции — когда функция определена так, что её значение для пр. набора (наборов) параметров неизвестно
В 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.
Формальная спецификация и верификация программ
|
|
