Program Analysis COP 5021
University of Central Florida
Popular in Course
Popular in Computer Programming
This 8 page Class Notes was uploaded by Luisa Beer on Thursday October 22, 2015. The Class Notes belongs to COP 5021 at University of Central Florida taught by Staff in Fall. Since its upload, it has received 69 views. For similar materials see /class/227468/cop-5021-university-of-central-florida in Computer Programming at University of Central Florida.
Reviews for Program Analysis
Report this Material
What is Karma?
Karma is the currency of StudySoup.
Date Created: 10/22/15
Dri Ferucio Laurentiu TIPLEA Visiting Professor School of Computer Science University of Central Florida CSB 205 Orlando FL 328162362 Tel 407 8231593 E mail tiplea cs ucf edu COP 5021 Program Analysis Spring 2006 Example denotational semantics of While programs Let S be the While program 11 while zl do yyz 12171 under the interpretation D N and Io 96 107 7 and 10n n for all n 2 0 Let 7 f L Then IS7 qb while z 1 do y y z 1 z 7217 mom1e 7a 71 do lty27 w z z 7 z 71vlyIo1 qb while z 1 do y y z 1 z 7 F7ly1l7 Where Ff7 is given by 0 Ffv f 1y I y I I I I 1W 7 ifIHI 171and Vii o FUW 7 72 ifIHz 71W 7 o and v 7 L o FUW 7 L 1w 7 L for any f E FL7FL and 7 6 FL Then 39 Ff7 f7ly7yVI z7 y7 y7 z 171 7 if 71 7g 1 and 7 f L Ff7 77 ifVI 1 and 7 f L 0 Ffv i7 if 7 L Let f0 LOHHFL be the least element of I L7J i ie the function given by f07 L for all 7 6 FL We know that MF supF f01n 2 We compute the elements of this chain 1 Mm 1 Ff07 7 if yz 1 1 if was y 1 and was y 2 F2fo7 y y 2111117 if WI 2 if 71 1 1 if was y 1 and was y 2 WWWy 2111117 if WI 2 7197y1111117 if 7 1 for any 7quot By mathematical induction we get n 7 i if7 zlt1ory zgtn F WW iwigMW21Mz1L if7 rjand1jn7 for any 7 and n 2 1 Then 7 1 if 7 z lt1 FW 7qyVy m 2 1z1 if was n 21 for any 7quot Substituting 7 by 7y1 we get 1 if z 1 MF7y1yy1n2111 iszzn21 for any 7 f 1 Then the semantics is MltSgtltvgt lf i ifdf m 11811 for any 7 For instance if 71 5 then MSy 1 5 6 4 6 3 6 2 11 Dri Ferucio Laurentiu TIPLEA Visiting Professor School of Computer Science University of Central Florida CSB 205 Orlando FL 328162362 Tel 407 8231593 E mail tiplea cs ucf edu COP 5021 Program Analysis This is the correctness proof for the speci cation Stack in Lecture Notes 4 Correctness We will prove that A is a member of ADTStaCk that is A is isomorphic to TEEi The rst step is to show that A is a model of the set E of equations in the speci cation stackp0pestack popAestackA PUMA estackA nack estack and A A WszacMPOMWSMIW p010 Push Mack 177alphy P0PPu5h75wck1v ValphW Papmzack 17azphy Vszack I KhanMI Therefore A is a model of the set E of equations of the speci cation De ne now the function f TEE HA such that the diagram in Figure 1 is commutative that is fsltlEs valAst7 for any sort 8 and term t of sort 8 fE is the natural epimorphism induced by Ei TE evalA A fE f T2E Figure 1 Graphic illustration of the isomorphism from T2E to A We show that f is an isomorphism o f is wellde ned 1ft and t are terms of sort 8 and t E5 t7 then tE5t gt EHt 42gt Ett gt ModE t 7 A t evalA5t evalA5t7 which shows that we fstEs o f is homomorphism 7 let 1 S i S n Then JamelWE fazphlte21EWgt 7 falph magma evalA lpMei A 7 for the term estack we have fswckestackTEE fsmckestackTEEstmk fstack65ta6kEstaak evalA5kaestac estack 7 if t1 is a term of sort stack and t is a term of sort alph7 then fSWCk puShTEE tlEs mk7 t2Ealph fstackqpuShTEt17t2Estmk fstackpu3htl7t2Estaak evalAstackpu3htl7t2 pushAevalA5wckt17evalAalpht2 PuShAfszackt1Esmk7falphat2Ewh 7 ift is a term of sort stack7 then f5tackltp0pTEEMEs mk fchPoPTEmamas fstackP0PtEsmk UalAstackp0p t P0PA valAszackt POPAfstacktEstmk o f is injective De ne rst the sets Calph 617 7en and Cnack push pushestacka1 7 ai E Calph U estack These sets satisfy l for any sort 8 and t 6 TE there exists 5 6 C such that t E5 c 2 for any 8 and 0102 6 C5 if evalA5cl evalA502 then cl 02 Now let 8 be a sort and t and t terms of sort 8 Then there exist 55 6 C5 such that t E5 c and t E5 cquot If we assume that f5tEs f5tES then evalA5c evalA5 c and c 5 therefore t E5 t which shows that f is inj ective o f is surjectz39ve 7 easily follows from the above constructioni As a conclusion A E ADTStaCki Dr Ferucio Laurentiu TIPLEA Visiting Professor School of Computer Science University of Central Florida CSB 205 Orlando7 FL 328162362 Tel 407 8231593 E mail tiplea cs ucf edu COP 5021 Program Analysis Spring 2006 Example denotational semantics of recursive programs Let 571 be the recursive program 51 F1z 5 ifz0then0else F2zil 7 F2z 5 ifz0thenlelse F1zil under the standard interpretation on Ni ie7 Di Ni The A terms associated to the program are T1 AF17F2Iif z 0 then 0 else F2z 7 and T2 AF17F2Iif z 0 then 1 else F1z 7 Their types are 7391 7392 natmat7 natmatgtnatgtnat7 and the corresponding domains are D71 D72 NLHNL gtlt NLHNLgtNLgtNLH The semantic function of the program is 109711T177IT277 Where 7 is an arbitrary but xed assignment The lest xed point of the semantic function is the supremum of the following chain L 510971 iNiaNi7iNiaNiln 2 0L Where JNL HNU is the least element of NLHNL that is7 the function Which maps each I 6 Ni to L Denote 0 f0 is the function JNL HNL 0 45157 1nfo7go fmgn7 for any n 2 07 Where go foi Moreover7 fn IT17fn17gn1 and 9n IT27fn1gn1 for any n 21 We have 130 ITl7f07yok 1T1VF1f01F2901HEk1 k 0 then 0 else 900i 1 ifk0then0else1 571k 1T27f0790k 1T271F1f011F290111k1 k 0 then 1 else f0k1 ifk0then1else1 IT17f1791k 1T1VF1f11F291111k1 k0then0 elseglk71 k0then0elseif k710then1else1 k0then0elseif k1then1else1 572k 1T2Vf1791k 1T2VF1f11F291111k1 i 0t en 1 e se 1 ifk0then1elseifk710then0else1 ifk0then1elseifk1then0else1 16306 IT1Vf2792k ITIVF1f21F292111k1 t en0elsegg k0then0elseif k710then1else k711then0else1 k0then0else k1then 1 else k2 then0else1 1020 573k 1T27f2792k 1T2VF1f2F2y2Hrk1 k 0 then 1 else f2 k0then 1 else k710then0else k711then1else1 k 0 then 1 else k 1 then 0 else k 2 then 1 else 1 for any h E N L By mathematical induction we can easily show that 07 if k lt n is even fnk 17 ifkltnis odd i7 otherwise 1 ifkltnis even 9706 0 if k lt n is odd 1 altfel foranyn21andkENii OW WOW supfmyn1n 2 0 7937 0 if k E N is even fk 1 ikaNis odd 1 ifk1 Where and 1 ikaNiseven 9k 0 ikaNisodd 1 ifk1 for any k E N L Therefore the denotational semantics of S 1 is 0 if k E N is even MIS1k 1 if k E N is odd unde ned if k 1 for any kENii