CS 421 Lecture 23: Hoare logic Lecture outline Proving properties of imperative programs Hoare logic Judgments, a.k.a. “Hoare formulas” AxiomsRules of inferenceRules of inference7/27/20091Review of last week Proof systems Formal frameworks for writing proofs Judgments, axioms, rules of inference Type systemsUsed for type checking, type inferenceUsed for type checking, type inference Judgments of the form: Operational semantics Used for proofs of correctness Judgments of the form: σ,η - e ⇓ v,σ′7/27/20092τ:e−Γ˫├Review: operational semantics Operational semantics of functional languages Based on expression evaluation Proofs follow the structure of the expression Variants OSsubst OSclo OSstate7/27/20093Examplelet f = fun x -> 3 in (f 1, f true)7/27/20094Today: proofs for imperative programs Hoare logic (or Hoare rules or Hoare formulas) Prove correctness of imperative programs Specifies pre- and post-conditions for statement execution Axiomatic semantics Contract principle7/27/20095Correctness of imperative programs Hoare formula says that if the variables in a program satisfy some properties, then after executing a given program, they satisfy some different properties. P {A} QExamples:Examples:x>0 { while ( x>0 ){y := y*x; x := x-1;} } y = y * x!x=x0& y=y0{ t := x; x := y; y := t } x=y0& y=x07/27/20096More examplestrue { if ( x<0 ) x := -x; } x = |x|true { n := length(a); b := [hd a];a := tl a;while (a != []) {while (a != []) {b = (hd a + hd b) :: b;a = tl a; }} (where bi= hd (tlib)and similarly for ak)7/27/20097∑−−==10inkkiabHoare logic Judgments: P {S} Q P, Q assertions about variables in the programS a statement in this language:S a statement in this language:Stmt -> Var := Expr | Stmt;Stmt| if (Expr) then Stmt else Stmt| while (Expr) Stmt7/27/20098Inference rules for Hoare logicP e}:{x P[e/x] =b & P S} (b) {while PP {S} b & P¬Q {S} PQQ'Q' {S} P'P' P⇒⇒7/27/20099b & P S} (b) {while P¬R }S ;{S PR }{S QQ }{S P2121Q {S} PQ }S else S then (b) {if PQ }{S b & PQ }{S b & P2121¬Rule of assignmentx+1=2 { x := x+1 } x=2P e}:{x P[e/x] =y=2 { x := y } x=27/27/200910Rule of assignment: examplesy=2 { x:=y } x=2y=2 { x:=2 } y=xx+1=n+1 { x:=x+1 } x=n+1x+1=n+1 { x:=x+1 } x=n+1x+1=n { x:=x+1 } x=nx+1=n { x:=x+1 } x=ntrue { x:=2 } x=27/27/200911Rule of consequenceQ {S} PQQ'Q' {S} P'P' P⇒⇒7/27/200912Rule of consequence: exampleQ {S} PQQ'Q' {S} P'P' P⇒⇒1nx1nxA1n1xnx+=⇒+=+=+⇒=7/27/2009131nx1}x:{xnx +=+==1nx1}x{x1n1x +=+=+=+A =Which inferences are correct? 25 x x}*x:{x3x25 x x}* x :{x 5 x & 0 x <==<=<>25 x x}* x :{x 3x<==7/27/20091425 x x}*x:{x5 x & 0 x 25 x x}* x :{x 3x<=<><==25 x x}*x:{x5 x & 0 x 25 x x}* x :{x 25 x*x<=<><=<Sequence ruleR }S ;{S PR }{S QQ }{S P21217/27/200915Sequence rule: exampleR }S ;{S PR }{S QQ }{S P2121&&0000yxxtBAxtxx=========7/27/200916&&&&&&&000000000000xyyxt}:y y;: xx;:{tyyxxxyyx};{yyxxyyxxx:tyyxx==================tyyxSequence rule: example&&&&000000yyyxxt}y : x{yyxxxt=======A =7/27/200917&&&&000000xyyxxt}t :y {yyyxxt=======B =If ruleQ }S else S then (b) {if PQ }{S b & PQ }{S b & P2121¬7/27/200918If rule: exampleQ }S else S then (b) {if PQ }{S b & PQ }{S b & P2121¬ ...x}:{x ... ...x}- :{x ... ⇒=⇒⇒=⇒7/27/200919|||0000x|x } x : xelse -x:then x 0 xif {xxx|x x}:{x0 x 0 x ...x}:{x ...x|xx}- :{x0 x 0 x ...x}- :{x ...&&===<===<¬====<==while ruleb & P S} (b) {while PP {S} b & P¬7/27/200920while rule: examples = 0; i = 0{ while (i< n) {b & P S} (b) {while PP {S} b & P¬{ while (i< n) {s := s+i;i := i+1;}7/27/200921ni & js 1i0j==⇒∑−=Comments on Hoare logic Proofs in Hoare logic are almost syntax-directed, i.e., almost have the same shape as the program being proved. The only exceptions are the uses of the rule of consequence.Applying Hoare rules is largely mechanical –given A and Applying Hoare rules is largely mechanical –given A and Q, most of the proof (including P) can be generated automatically. Creativity is required mainly in determining the invariant in a while loop, because Q may not have the form “P & ¬b”. A formula of that form needs to be found (after which the rule of consequence can be used, proving P & ¬b ⇒ Q).7/27/200922Example: gcd algorithma > 0 & b > 0 & a=a0& b=b0{while (a ≠ b)if (a > b) then a := a − b;else b := b − a;} a = gcd(a0, b0)} a = gcd(a0,
View Full Document
Unlocking...