МФСП, 09 лекция (от 29 октября)
Материал из eSyr's wiki.
- Диктофонная запись: http://esyr.org/lections/audio/mfsp_2008_winter/MFSP_08_10_29.ogg
Консультация
В каждом билете должно быть 4 задачи. Теоретического материала никакого нет.
- Либо перевод явной спецификации в неявную. Спецификации должны быть абсолютно эквивалентны. Любые неточности будут трактоваться как ошибки. Могут быть погрешности практического плана, это не беда. Если же искажена семантика, то это ошибка. Иногда включается обрб. трансляция, но это случай редкий. Тут рассматривается одна функция.
- Даётся алгебраическая спецификация, и по ней необходимо дать явную, неявную спецификацию группы функций, чтобы в них были определены предусловия, и все спецификации должны отвечать требованиям аксиом, сформулированным в задаче. Тут группа функций рассматривается. Для каких-то функций можно использовать явную, для каких-то — неявную спецификацию, на выбор.
- Даётся алгебраическая спецификация, плюс даётся явная спецификация. Надо доказать, что явная спец. явл. или не является уточнением алгебраической.
- Упрощение некоего выражения. В качестве выражения даётся фрагмент спецификации, в котором активно используется параллельность, внутренний/внешний выбор, взаимная блокировка, и так далее.
Содержание |
[править] Конкретные примеры
[править] 1. (Билет 1 задание 1 из методички 2008)
f: Int × Int × Int → write x read y Int × Int
f(a,b,c) ≡; if a=b then
(if a+b > c then c else a+b end,
a*b*(if c>0 then x:=y; c else 0-c end))
else (a+b, x:=b; a-b)
end
Подводные камни:
- Никогда нет присваивания.
- В случае неизменённых переменных на запись в постусловии надо написать, что значение переменной сохраняется: x=x'
- Выражение должно быть корректно
Ответ:
f: Int × Int × Int → write x read y Int × Int
f(a,b,c) as (d, e)
post
if a=b then
if a+b>c then
if c>0 then
d=c ∧ x=y ∧ e = a*b*c
else
d=c ∧ x=x’ ∧ e=a*b*(0-c)
end
elseif c>0 then
d=a+b ∧ x=y ∧ e= a*b*c
else
d=a+b ∧ x=x‘ ∧ e=a*b*(0-c)
end
else
d=a+b ∧ x=b ∧ e=a-b
end
Для каждой комбинации входных данных выписывается результат в том или ином случае. Результат состоит из d, e и x.
Где подобная задача может встретиться: в переписывании legacy, как альтернатива реверс-инжинирингу.
Перевод из неявной спецификации в явную это обычное программирование.
[править] 2. (Билет 1, задание 2)
type S, E
value create : Unit → S, add : E × S → S, del : S -~-> S, next : S -~-> S, get : S -~-> E, append : S × S → S
axiom
∀ e : E, s : S :- del(add(e, s)) ≡ s,
∀ e : E, s : S :- get(add(e, s)) ≡ e,
∀ e : E, s : S :- next(add(e, s)) ≡
if s = create() then
add( e, s )
else
append ( s, add( e, create( ) )
end,
∀ e : E, s1, s2 : S :- append(create(), s2)) ≡ s2, ∀ e : E, s1, s2 : S :- append(add(e, s1), s2)) ≡ add(e, append (s1, s2))
Всегда на входе будет группа функций, работающая с общей структурой данных. При этом, видимо, E — элемент, S — структура. При этом внутреннее представление элемента не важно, а вот что за S, хорошо бы догадаться. Какие бывают виды структур: множество, список, отображение. Элементами его могут быть или сами элементы E, множества, списки, отображения. Помимо совсем простых, базовых структур, может быть более хитрая структура, например, круговой список. Структура может быть необязательно одноуровневой Т. о.с совет: сначала понять, какая структура данных скрыта за спецификацией, и после этого писать спецификацию.
Ответ: видимо, S это кольцевой список.
type
E,
S : E-l≡t
value
create : Unit → S
create ≡ <..>,
add : E × S → S
add (e,s) ≡ <.e.> ^ s,
del : S -~-> S
del (s) ≡ tl s
pre s ≠ <..>,
next : S -~-> S
next (s) ≡ tl s ^ <. hd s .>
pre s ≠ <..>, /* Надо писать предусловие */
get : S -~-> E
get (s) ≡ hd s
pre s ≠ <..>,
append : S × S → S
append (s1, s2) as s
post
if s1=<..> then s=s2
else s=add(hd s1, append( tl s1, s2))
end
[править] 3. Доказательства
Самое длинное решение.
Какие правила:
- Вычислять всё, что можно вычислить
- Подстановка. Всегда в качестве условия даётся явное определение. Везде, где в алгебраической спецификации вы видите обращение к функции, в этом месте всегда можно сделать подстановку
- Базовые операции с основными структурами данных в случае известных значений.
Для каждой из аксиом проводятся преобр. для правой и левой части, пока либо они нне станут текстуально равны, либо пока они не станут явно неэквив.
Может в условии задач слегка ошибиться и можно увидеть по сигнатуре, что они не являются уточнением. Если такая ошибка найдётся, то ваше счастье.
Если запись будет не слишком подробной, то это нормально
[править] 4. Задачи на упрощение
Какие бывают типы:
- ||, П
- ||, ++
- ||, []
Более хитрых комбинаций быть не должно.
(b!2) || (y := a?) || if (x:=1); (a!x); (true П false) then a!(b?) else a!(1+b?) end
Финальная запись решения, это, как правило, набор выражений, различающихся внутренним выбором, каждое из них достаточно простое.
Для начала просканировать и найти контрагентов.
- Первый тред пишет b? второй читает
- Второй тред взаимодействует с оператором (a!x) из третьего треда
a!(5+b?) || ((x:=(if true П false then x:=b?;1 else b!3; x:=2; 6 end) +x) ++ (b!4|| y:=b?))
По поводу: (x:=a?)||(x:=b?). Мы ничего не можем сказать без окружения. Если это изолированный оператор и ничего в каналах нет, то это бесконечное ожидание. Если порядок получения данных из каналов известен, то мы можем сказать что-то определённое, если же порядок неизвестен, то и сказать ничего не можем.
Может ли провзаимодействовать 5+b? и b!3 ? Только если после взаимодействия в интерлоке это взаимодействие не используется и оно будет выполнено, то да.
- Рассмотрим первые два случая: a!(5+b?) || ((x:=((x:=b?;1)П(b!3;x:=2;6))+x)||(y:=4)). Поскольку все взаимодействия произошли, то ++ заменяется на ||.
- a!(5+b?) || ((x:=(x:=b?;1)+x)||(y:=4)) — первое решение
Больше выписывать не будем.
Варивант со внешним взаимодействием: почти наверняка это будет case:
case (1 П b?) of 1: 3: 5: end || a! ... || b!(a?+2) || ...
Результатом будет ветка кейса и те взаимодействия, которые не заверш..
Организационные замечания:
- Можно пользоваться молча любыми источниками информации
- Нельзя обмениваться информацией ни в каком виде
Результирующая оценка за предмет будет состоять из двух коллоквиумов и, возможно, оценки по успехам за практическое задание.
Формальная спецификация и верификация программ
|
|
