МФСП, 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) || ...
Результатом будет ветка кейса и те взаимод., которые не заверш..
Орг. замечания:
- Можно польз. молча любыми ист. информации
- Нельзя обмениваться информацией ни в каком виде
Результ. окзенка за предмет будет сост. из двух коллоквиум и возм. оценка по успехам за практ. задание.
Формальная спецификация и верификация программ
|
|
