南京大学：《程序设计语言的形式语义》课程教学资源（课件讲稿）07_Axiomatic Semantics and Hoare Logic

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