Решения задач МСФП.

Решения задач МСФП. Составлял Николай Князев на основеразбора задач, проводимого Михаилом Балюком 19.12.09.Вопросы присылайте rumata@angel.cs.msu.su version 1.2 от 21.12.09 15:15Первая задача по явному описанию функций построить пост-условия для всех. Важно: в пост-условиях не должно быть локальных переменныхF: intXInt -> write x,y,z intxintxintf(a,b) as (c,d,e)f(a,b) is x=2local variable v int :=1 infor i in <a...a-1+b>inv:=i*(x=x+v;)i*2 (ЗДЕСЬ v не успевает обновиться,т.е идет с предыдущего цикла, т.е. Для x последнейитерацией (где v=a-1+b) нет)end;(y:=z;a,v:=v+1;x,b+v)Необходимо помнить формулыcуммы арифм и геом прогрессиx=2A  Akn−1Sn = k2nB 1−q Sn = 11−q1=b>b<1но в нашей задаче мы имеемcумму квадратов арифм.прогрессии.

Формула извикипедии для 1..kk(k+1)-(2k+1)/6V=(a-1+b)²*2Надо учесть, чтоx=3 на первойитерации, таким образом для x:x=32Sa− 2 b−2S ay=z´c=ad=ze=e+2x=2z=z´(важно,все писать!)с=ad=xe=b+v+1y=z´x=32Sa− 2 b−2S aОтвет, это пост-условие(b<1 /\ y=z´ /\ с=a /\ d=z /\ e=b+2 /\ x=2 /\ z=z¨)\/(b>=1/\ c=a/\d=(здесь расписываем x)/\e=b+(a-1+b)*(a-1*b)*2+1)Задача 2Дана алгебраическая спецификация набора функций, нужнопереписать все в явном или неявном, но проще в явном ;).Карныхин обещал, что задачи будут как на форуме и попроще, что можнорешить пристальным взглядом.(набор функций это все булевы выражения, т.е.

Если нет знака ´=´ значитэта штука должна быть true а ´~´ значит отрицание)Задачаtype E, Tvalue empty: Tput: TxE -> Tchech T->boolput (put(t,x),y)is put(put(t,y),x)check(empty)~check(put(empty,x))check(put(put(empty,x),y)is(x~=y)check(put(put(t,x),x)is check(put(t,x))~check(put(put(t,x),y)) pre x~=y /\ put(t,x)~=t /\/\ put(t,y)~=t /\ ~check(t)РешениеВозникла идея от Степы - сheck, это проверка на четность числа разныхэлементов, посмотрим что означают написанны аксиом:check(put(put(empty,x),y)is(x~=y) — (т.е.

По суте Положили вмн-во два элемента разных сheck - true)~check(put(put(t,x),y)) pre x~=y /\ put(t,x)~=t /\/\ put(t,y)~=t /\ ~check(t) — если добавление двух новыхэлментов то чек не изменилсяпереписываем явноtype E, T = E servalue empty: Tput: TxE -> Tcheck T->boolput (t,e) is t union {e}check (t) is ((card t)\2)=0)Задача на ЭТО (№ 4) и проверять их будет только Лекторусловие игра в пятнашки преобразить в рсл, приведены часть спецификаций и(описание игры здесь его не переписываю)Nat4={|n:Nat:-<=/\n>0|} - мн-во нат чисел 1..4Nat15={n:Nat:-n<=5/\n>0} —Square=(Nat4xNat4xNat15)-set — мн-во состоящие из троек чиселvaluemove Square x Nat4x Nat4 -~ ->Squarenew game Unit ->square (Unit это пустой тип)Функция move берет поле и сдвигает клетку на пустую — получаем поле1.

подумать и написать все ограничения на русском языке.Ограничения на Square не более 15 фишекforall s : Square :- card s = 15в S (x,y,x) нет троек с одинаковым 3-му параметром(номер пятнашки), в s нетэлементов у которых одновременно равны 1 и2й параметры(находятсяодновременно на одной позиции)ограничения для movepre: рядом должна быть пустая клеткаpost: поменялось положение только одной пятнашкиесли это все написать, то уже 1 балпишем теперь формально на rsl:newgame() as spost forall z:Nat15 :- if exists x,y:Nat4 :- (x,y,z) isin S then ~exist s x1 y1:Nat4:(x1,y1,z)isin S/{(x,y,z)} /\ (анаглогично условие на уникальноссть места) ( лекторсказал что можно писать в похожих случаях слово ¨аналогично¨)move (s,x,y ) as S1post [ exist t : Nat15 :- (x,y,t) isin S /\ exists x1,y1:Nat4 :- (x1,y1,t) isin S1 /\/\ (x=x1/\abs(y-y1)=1 \/ y=y´/\ abs (x-x1)=1 ) /\ s\(x,y,t)=s1/\(x1,y1,t) ] /\ forallt1:Nat15:-(x,y,t1)~isin S1( второй вариант постусловия что-то типа card (s1\s2) /\ card(s\s1 = 1) /\ ...)pre forall z:Nat15:-((x-1,y,z)~isins/\x>1)/\аналогично для остальныхaxiomforall s : Square :- (card s = 15)/\forall z:Nat15 :- if exists x,y:Nat4 :- (x,y,z) isin S then ~exist s x1 y1:Nat4:(x1,y1,z)isin S/{(x,y,z)} — условие на уникальность номеров фишеканалогично расписать уникальнось местАксимоы и постусловия функции newgame — совпадают с точностью до символа,т.к.

И то и то, есть ограничения на поле для игры.Задача 6. будет задача как в праке и доказать через PVSлегко это с ноутом без него сделать, считает Миша, нереально. Есть наборкоманд кот можно юзать.Но попробуем.антецендент сверхуконсиквент снизув общем случае-1 a1узел верен если верно следствие-2 a2a1/\a2/\а3=>u1\/u2\/u3-3 a3-------1 u12 u23 u3условие задачи:task Theorybeginsum2(n:nat):recursive nat =if n=0 then 0 else n*(n-1)+sum2(n-1) elseifmeasure nsun2_theorem: theoremforall (n:nat):(n>=2) implies sum2(n)=(n-1)*n(n+1)/3End taskБазаиндукции0>=2=>..flatten 1(Induct 1)Forall n in nat:n>=2 =>sum2(n)Forall n S(n)=>S(n+1)skolem 10>=2asserttrueInduct — делит доказывемое утвердение на базу и индуктю переходflatten - делит так, чтобы из правды не следовала ложь, т.е антедент наверх и true а кfalseskolem разбивает forall делает подстановку.

(сразу его сделать не можем, т.к. У на Nat)assert — проверка на очевидную верность полученного утвержденияДаже при помощи ноута и pvs решить задачу нам не удалось, более того врезультате преобразований мы получили не верное утверждение, хотя условиебыло переписано верно а преобразования проводились на ноуте. Что делать втаких случаях непонятно.Общие слова по третей задачи аксиомы и реализации нужно проверитьявляется ли вторая уточнением первой.

Мы должны подставлять функции извторой в аксиомы пока не докажем что все ок НО много где получается чтовторая не является уточнением. Нужно приводить контр-пример. Придуматьнабор переменных такие, что не выполняются аксиомы. Есть доходчивыепримеры как доказыать, если оно является уточнением.Задача 4 с помощью метода Флойда доказать полную корректностьесть блок-схема программы, доказать что из описанногопредусловия φ следует описанное постусловие ΨSTART(y1,y2)<-(x,1)T2y2<=xA (точка сечения)Fy2<xFTHALTz<-y1(y1y2)<-(2y1,2y2)(y1y2)<-(y1+x,y2+1)Дано: Предусловие φ=(x>=0) постусловие Ψ=(z=x²)в блок-схеме существуют входные параметры (х и 1 в нашем случае), они не изменяютсяв процессе выполнения, промежуточноые у1 и у2 и выходные их пишем только в конце z.Для доказательства полной корректности по методу Флойда надо доказать частичнуюкорректнось и завершаемость.Нужно выбрать точки сечения: это начало и конец программы +хоть одна точка вкаждом цикле.Нужно придумать предикаты, которые правдивы в точках сечения и из них ипредусловия должно следолвать постусловияпредикаты придумываются пристальным взглядом+можно попробовать посчитать прогуна конкретных числах.Придумали y1 = x*y2нужно для всех путей между точками сечения проверить наши предикатыесть пути между точками сечения.

Присваем y1= x*y2 должны проверитьS-A(x>=0 => x=x*1A-T-T-A  (y1=x*y2)/\(y2<x)/\(2y2<=x))=>2y1=x*2y2A-T-F-A y1=xy2/\....=>(y1+x=xy2+x)A-F-H (y1=xy2)/\ ((y2>=x)\/(x=0))=>z=x² (т.к. Одновременно z=y1=xy2 и x=<y2<x)то, что написан красным мы придумали вставить в предикат потом, по хорошему нужнотогда доказать прадивость всего получившегосяэ предиката (y1=xy2)/\ ((y2>=x)\/(x=0)для всех путей.

частичная коррекктность доказаназавершаемость доказываем методом фундированных множеств. Т.е. Мн-во ЧУМ где несуществует бесконечно убывающей последовательности положительных чисел.Надо написать:W=Nat, < (т.е мы берем мн-во натуральных чисел, с операцией <)мы должны напистать, что когд U станет меньше 0, мы пришли в конец в нашем случаеU(x...y)=x-y2, и если она убывает то рано или поздно будет меньше 0, Мише такое зачли,но хз как будет проверять Карныхин..