CS266 - Formal Specification and VerificationWinter 2009Homework #2 -Symbolic Execution HomeworkDue: Tuesday 20 JAN 09, 11:00am1. Consider the following program which divides x by y and returns the quotient in quot and theremainder in rem.1procedure divide(x,y:integer; var quot,rem:integer);2begin3{:assume ((x>=0) & (y>0)) :}4quot := 0;5rem := x;6{:assert ((x=quot*y + rem) & (rem>=0) & (x=x’) & (y=y’)) :}7while rem >= y do begin8quot := quot + 1;9rem := rem - y10 end11 {: prove ((x’=quot*y’ + rem) & (rem>=0) & (rem<y’)) :}12 end;Verify that this program is correct with respect to its input and output assertions as I did for the exam-ples in class. That is, Drawthe symbolic execution tree and generate each of the verification conditions(You may prove them if you want.).2. Choose aprogram of your liking that contains at least one loop. Your program should be of thesame complexity as the factorial example that I presented in class. Forthis program you are to do the fol-lowing:a) Give Entry and Exit assertions that properly describe the function of the program.b) Give a loop assertion for each loop in the program.c) Verify that your program is correct with respect to its entry and exit assertions by using thesymbolic execution rules that I presented in class. (Drawthe symbolic execution tree(s) for the verificationof your algorithm.)If you need anyaxioms about the integers, such as were needed for the factorial algorithm, you should statethe necessary axioms.3. Give a symbolic execution rule for the Pascal repeat statement.repeat <statement-list> until <Boolean expression>-2-4. A verification condition is generated for each path in the program that starts at an assertion (i.e.,an assume or assert statement) and ends at an assertion (i.e., an assert or prove statement).Consider the following program which multiplies a by b and returns the product in prod.1procedure multiply(a,b:integer; var prod:integer);2var3tema, temb, s: integer;4begin5{:assume (true) :}6tema := a;7prod := 0;8{:assert ((prod=(a-tema)*b) & (a=a’) & (b=b’)) :}9while tema <> 0 do begin10 if tema > 0 then11 s := 112 else13 s := -1;14 temb := b;15 {: assert ((prod=(a-tema)*b + s*(b-temb))&(a=a’) & (b=b’)) :}16 while temb <> 0 do17 if temb > 0 then begin18 prod := prod + s;19 temb := temb - 120 end21 else begin22 prod := prod - s;23 temb := temb + 124 end;25 tema := tema - s26 end27 {: prove (prod=a’*b’) :}28 end.Forthis program I would likeyou to indicate each of the paths for which a verification condition isgenerated. The paths should be denoted by a sequence of line numbers (eg., 5,6,7,8).Iwould also likeyou to generate the verification condition for all paths that include line