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=ee<ee>e -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 | 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