This preview shows page 1-2-3-4-5-6-7-8-9-10-11-12-13-14-95-96-97-98-99-100-101-102-103-104-105-106-107-192-193-194-195-196-197-198-199-200-201-202-203-204-205 out of 205 pages.
CS378 - A Formal Model of the JVMLectures 6,7,8http://www.cs.utexas.edu/users/moore/classes/cs378-jvm/Semester Spring, 2012Unique Id 53105Intructor J Stroth e r MooreEmail moor [email protected] MAI 2014Office Hours MW 1:00–2:001Review M1 Release on Web2Two Flavors of CorrectnessPartial:If computation on ok inputs halts, then theanswer is as expected.Total:Computation from ok inputs halts and theanswer is as expected.3State-Based FormalizationThe most general way to formulate theseconditions is in terms of entire M1 states.(pre si) – checks that siis an acceptab l einitial state for your program(post sisf) – ch ecks that the final state,sf, i s in the expected relation with theinitial state si4(halted sf) – checks that state sfishalted, e.g. , (next-inst sf) = ’(HALT)5Most-General State Based PartialCorrectness∀ si, σ :((pre si)∧(halted (run σ si))→(post si(run σ si))6Most-General State Based TotalCorrectness∀ si∃ σ :(pre si)→((halted (run σ si))∧(post si(run σ si)))7However...It is gener a ll y more conveni en t to relateprogram inputs and outpu ts rather thanwhole states.So for the next few l ectur es we dea l withslightly less general notions of correctness...8Typical Idioms in M1 CorrectnessStatements• the in itia l state, sometimes called siandoften wr i tten(make-state 0 (list v1. . .) nil π)• the acceptab l e val ues of the inpu ts (localvariabl es), v1, . . ., e.g., (natp v1)• the sched ule, σ, sometimes kn own andsometimes not9• the final state, sf, usually just(run σ si)• where in th e final state the answer isfound, e.g., (top (stack sf))• the expected answer θv1,..., i.e. , so meexpression in terms of the in p uts, e.g.,(* v1v2).10Partial Correctness“If computation on ok in p uts ha l ts, thenthe an swer is as expected.”( si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run sched si)∧ (next-inst sf) = ’(HALT))→(top (stack sf)) = θ.11Partial Correctness“If computation on ok in p uts ha l ts, thenthe an swer is as expected.”( si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run sched si)∧ (next-inst sf) = ’(HALT))→(top (stack sf)) = θ.You may elimin ate equality hypotheses tha tjust “name” expressions.12Partial Correctness( si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run sched si)∧ (next-inst sf) = ’(HALT))→(top (stack sf)) = θ.13Partial Correctness(∧ (ok-inputs v1. . .)∧ sf= (run sched(make-state 0 (list v1. . .)∧ (next-inst sf) = ’(HALT))→(top (stack sf)) = θ.14Partial Correctness( (ok-inputs v1. . .)∧ sf= (run sched(make-state 0 (list v1. . .) nil π))∧ (next-inst sf) = ’(HALT))→(top (stack sf)) = θ.15Partial Correctness( (ok-inputs v1. . .)∧sf= (run sched(make-state 0 (list v1. . .) nil π))∧ (next-inst sf) = ’(HALT))→(top (stacksf)) = θ.16Partial Correctness( (ok-inputs v1. . .)∧ (next-inst(run sched(make-state 0 (list v1. . .) nil π)))= ’(HALT))→(top(stack(run sched(make-state 0 (list v1. . .) nil π))))= θ.17Partial Correctness(si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run sched si)∧ (next-inst sf) = ’(HALT))→(top (stacksf)) = θ.18Partial Correctness (in ACL2)(implies(and(equal si(make-state 0 (list v1. . .) nil π))(ok-inputs v1. . .)(equal sf(run sched si))(equal (next-inst sf) ’(HALT)))(equal (top (stack sf)) θ))19Total Correctness“Computation from ok inputs halts and th eanswer is as expected.”∃ σ :( si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run σ si))→( (next-inst sf) = ’(HALT)∧(top (stack sf)) = θ).20Total Correctness (in ACL2)“Computation from ok inputs halts and th eanswer is as expected.”∃ σ :(implies(and(equal si(make-state 0 (list v1. . .) nil π))(ok-inputs v1. . .)(equal sf(run σ si)))(and (equal (next-inst sf) ’(HALT))(equal (top (stack sf)) θ)))21Total Correctness (in ACL2)“Computation from ok inputs halts and th eanswer is as expected.”∃ σ :(implies(and(equal si(make-state 0 (list v1. . .) nil π))(ok-inputs v1. . .)(equal sf(runσ si)))(and (equal (next-inst sf) ’(HALT))(equal (top (stack sf)) θ)))22Total Correctness (in ACL2)“Computation from ok inputs halts and th eanswer is as expected.”(implies(and(equal si(make-state 0 (list v1. . .) nil π))(ok-inputs v1. . .)(equal sf(run(sched v1. . .) si)))(and (equal (next-inst sf) ’(HALT))(equal (top (stack sf)) θ)))23Total Correctness“Computation from ok inputs halts and th eanswer is as expected.”∃ σ :( si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run σ si))→( (next-inst sf) = ’(HALT)∧(top (stack sf)) = θ).24Total Correctness“Computation from ok inputs halts and th eanswer is as expected.”∃ σ :( si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run σ si))→((next-inst sf) = ’(HALT)∧(top (stack sf)) = θ).25Bogus Correctness“Computation from ok inputs produces theanswer expected.”∃ σ :( si= (make-state 0 (list v1. . .) nil π)∧ (ok-inputs v1. . .)∧ sf= (run σ si))→(top (stack sf)) = θ.26Demo 127We Will Focus on Total Correctness∃ σ :( si= (make-state 0(list v1. . .)nilπ)∧ (ok-inputs v1. . .)∧ sf= (run σ si))→( (next-inst sf) = ’(HALT)∧(top (stack sf)) = θ).28We Will Focus on Total Correctness∃ σ :( si= (make-state 0(list v1. . .)nilπ)∧ (ok-inputs v1. . .)∧ sf= (run σ si))→( (next-inst sf) = ’(HALT)∧(top (stack sf)) = θ).29We Will Focus on Total Correctness( si= (make-state 0(list v1. . .)nilπ)∧ (ok-inputs v1. . .)∧ sf= (run (sched v1. . .) si))→( (next-inst sf) = ’(HALT)∧(top (stack sf)) = θ).30Recall(defconst *g-program*’((ICONST 0) ; 0(ISTORE 2) ; 1 a = 0;(ILOAD 0) ; 2 [loop:](IFEQ 10) ; 3 if x=0 then go to end;(ILOAD 0) ; 4(ICONST 1) ; 5(ISUB) ; 6(ISTORE 0) ; 7 x = x-1;(ILOAD 1) ; 8(ILOAD 2) ; 9(IADD) ;10(ISTORE 2) ;11 a = y+a;(GOTO -10) ;12 go to loop(ILOAD 2) ;13 [end:](HALT))) ;14 ‘‘return’’ a31GoalLet’s specify an d prove the totalcorrectness of *g-program*, namely, thatthe expected r esult is the product of thetwo inputs.32Total Correctness of *g-program*( si= (make-state 0(list x y)nil*g-program*)∧ (ok-inputs x y)∧ sf= (run (sched x y) si))→( (next-inst sf) = ’(HALT)∧(top (stack sf)) = (* x y)).33Total Correctness of *g-program*( si= (make-state 0(list x y)nil*g-program*)∧(ok-inputs x y)∧ sf= (run (sched x y) si))→( (next-inst
View Full Document
Unlocking...