Решения задач МСФП. (1185152)
Текст из файла
Решения задач МСФП. Составлял Николай Князев на основеразбора задач, проводимого Михаилом Балюком 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 Akn−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=32Sa− 2 b−2S ay=z´c=ad=ze=e+2x=2z=z´(важно,все писать!)с=ad=xe=b+v+1y=z´x=32Sa− 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, Мише такое зачли,но хз как будет проверять Карныхин..
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
