Axiomatic Semantics and Hoare Logic (Slides modified from Mike Gordon,Hongjin Liang) 11197
Axiomatic Semantics and Hoare Logic (Slides modified from Mike Gordon, Hongjin Liang) 1 / 197
Outline Program Specifications using Hoare's Notation Inference Rules of Hoare Logic Automated Program Verification Soundness and Completeness Discussions 2/197
Outline Program Specifications using Hoare’s Notation Inference Rules of Hoare Logic Automated Program Verification Soundness and Completeness Discussions 2 / 197
Floyd-Hoare Logic This class is concerned with Floyd-Hoare Logic also known just as Hoare Logic Hoare Logic is a method of reasoning mathematically about imperative programs It is the basis of mechanized program verification systems Developments to the logic still under active development,e.g. separation logic(reasoning about pointers) concurrent program logics 3/197
Floyd-Hoare Logic This class is concerned with Floyd-Hoare Logic I also known just as Hoare Logic Hoare Logic is a method of reasoning mathematically about imperative programs It is the basis of mechanized program verification systems Developments to the logic still under active development, e.g. I separation logic (reasoning about pointers) I concurrent program logics 3 / 197
A simple imperative language (IntExp)e ::n x I e+el e-el... (BoolExp)b ::true false e=eee -b bAb l bvb l .. (Comm）c:= skip x:=e 1 C;C L if b then c else c while b do c (State)σeVar→lnt 4/197
A simple imperative language (IntExp) e ::= n | x | e + e | e − e | . . . (BoolExp) b ::= true | false | e = e | e e | ¬b | b ∧ b | b ∨ b | . . . (Comm) c ::= skip | x := e | c ; c | if b then c else c | while b do c (State) σ ∈ Var → Int 4 / 197
Outline Program Specifications using Hoare's Notation Inference Rules of Hoare Logic Automated Program Verification Soundness and Completeness Discussions 5/197
Outline Program Specifications using Hoare’s Notation Inference Rules of Hoare Logic Automated Program Verification Soundness and Completeness Discussions 5 / 197
Specifications of imperative programs Acceptable Acceptable Initial State Final State “Xis “Y is the greater than square root Zero” Action ofX” of the Program 6/197
Specifications of imperative programs 6 / 197
Hoare's notation(Hoare triples) For a program c, partial correctness specification: (p)ciq) total correctness specification: [p]c[q] Here p and g are assertions,i.e.,conditions on the program variables used in c. p is called precondition,and q is called postcondition Hoare's original notation was plc)q not (p)c(q),but the latter form is now more widely used 7/197
Hoare’s notation (Hoare triples) For a program c, I partial correctness specification: {p}c{q} I total correctness specification: [p]c[q] Here p and q are assertions, i.e., conditions on the program variables used in c. I p is called precondition, and q is called postcondition Hoare’s original notation was p{c}q not {p}c{q}, but the latter form is now more widely used 7 / 197
Meanings of Hoare triples A partial correctness specification (p)c(g)is valid,iff if c is executed in a state initially satisfying p and if the execution of c terminates then the final state satisfies g It is "partial"because for (p)clg)to be true it is not necessary for the execution of c to terminate when started in a state satisfying p It is only required that if the execution terminates,then g holds 8/197
Meanings of Hoare triples A partial correctness specification {p}c{q} is valid, iff I if c is executed in a state initially satisfying p I and if the execution of c terminates I then the final state satisfies q It is “partial” because for {p}c{q} to be true it is not necessary for the execution of c to terminate when started in a state satisfying p It is only required that if the execution terminates, then q holds 8 / 197
Meanings of Hoare triples A partial correctness specification (p)clg)is valid,iff if c is executed in a state initially satisfying p and if the execution of c terminates then the final state satisfies q A total correctness specification [p]c[q]is valid,iff if c is executed in a state initially satisfying p then the execution of c terminates and the final state satisfies g Informally:Total correctness=Termination Partial correctness 9/197
Meanings of Hoare triples A partial correctness specification {p}c{q} is valid, iff I if c is executed in a state initially satisfying p I and if the execution of c terminates I then the final state satisfies q A total correctness specification [p]c[q] is valid, iff I if c is executed in a state initially satisfying p I then the execution of c terminates I and the final state satisfies q Informally: Total correctness = Termination + Partial correctness 9 / 197
Examples of program specs {x=1} X:=X+1 {x=2} valid {x=1 X:=X+1 {x=3} invalid 10/197
Examples of program specs {x = 1} x := x + 1 {x = 2} valid {x = 1} x := x + 1 {x = 3} invalid {x − y > 3} x := x − y {x > 2} valid [x − y > 3] x := x − y [x > 2] valid {x ≤ 10} while x , 10 do x := x + 1 {x = 10} valid [x ≤ 10] while x , 10 do x := x + 1 [x = 10] valid {true} while x , 10 do x := x + 1 {x = 10} valid [true] while x , 10 do x := x + 1 [x = 10] invalid {x = 1} while true do skip {x = 2} valid 10 / 197