Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 1An Axiomatic Basis for Computer ProgrammingC.A.R. HoareHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 2Hoare’s Axiomatic Semantics“An Axiomatic Basis for Computer Programming", CACM , 1969“Procedures and Parameters: An Axiomatic Approach,” Proceedings of the Symposium on Semantics of Algorithmic Languages, 1971“Proof of Correctness of Data Representations,”Acta Informatica, 1972Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 3An Axiomatic Basis for Computer Programming• Provided the basis for proving programs correct with respect to their specifications• Introduced the P{Q}R notation• Based on earlier work by Floyd (1967), which was applied to flowcharts• Presented a set of axioms for computer arithmeticHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 4An axiomatic definition serves as a:• Contract between a language designer and an implementer• Reference manual for a programmer• Axiomatic basis for formal proofs of properties of programsHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 5Axiomatic definition comprises a deductive system• Axioms defining the primitive constructs of the language• Rules of inference• Underlying logical system (e.g., first order predicate calculus with equality)Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 6Axioms for Integer Arithmetic• Standard arithmetic axioms• Axioms for the finite arithmetic of computers– Strict interpretation– Firm boundary– Modulo arithmeticHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 7Some Axioms for IntegersA1 x+y = y+xA2 x*y = y*xA3 (x+y)+z = x+(y+z)A4 (x*y)*z = x*(y*z)A5 x*(y+z) = x*y + x*zA6 y ≤ x → (x-y) + y = xA7 x+0 = xA8 x*0 = 0A9 x*1 = xHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 8• Finite Arithmetic∀x (x ≤ max)• Overflow– strict interpretation~∃x (x = max + 1)– firm boundarymax +1 = max– modulo arithmeticmax + 1 = 0Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 9Strict Interpretation+ 0 1 2 30 0 1 2 31 1 2 32 2 33 3* 0 1 2 30 0 0 0 01 0 1 2 32 0 23 0 3Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 10Firm Interpretation+ 0 1 2 30 0 1 2 31 1 2 32 2 33 3* 0 1 2 30 0 0 0 01 0 1 2 32 0 23 0 3Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 11Modulo Interpretation+ 0 1 2 30 0 1 2 31 1 2 32 2 33 3* 0 1 2 30 0 0 0 01 0 1 2 32 0 23 0 3Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 12Partial Correctness NotationP{Q}RP,R are predicatesQ is a program or piece of codeIf the assertion P is true before initiation of program Q, then assertion R will be true on its completionHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 13More Notation|- TheoremhoodReRe →→→→x H1, H2, …. , Hnwhenever H1 through HnHn+1 are true Hn+1 is truexHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 14D0: Axiom of Assignment Pe{x:=e}PExample:y>8 {x := y + 4} x>12xHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 15Hoare’s Proof Technique• Uses sentences of the form P{S}Q• A proof of a sentence P{S}Q is a sequence of sentences the last of which is P{S}Q• Where each sentence is:– an instantiation of an axiom– a theorem in the underlying logical system– follows from previous lines by applying a rule of inferenceHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 16D1: Rules of ConsequenceP{Q}R, R→S P{Q}R, S→PP{Q}S S{Q}RHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 17D2: Rule of CompositionP{Q1}R1, R1{Q2}RP{Q1; Q2}RHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 18PROCEDURE TEST (A, B: INTEGER;VAR X, Y, Z: INTEGER);BEGINX := A + B;Y := A - B;Z := X + YEND;ENTRY: true EXIT: X = A + B & Y = A - B & Z = 2AHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 19D3: Rule of IterationP & B{S}PP {while B do S} ~B & PHoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 201 PROCEDURE FACT ( N:INTEGER; VAR Y:INTEGER);2 VAR X: INTEGER;3 BEGIN4 X := 0;5 Y := 1;6 ASSERT ( Y = X! & X ≤ N )7 WHILE X < N DO BEGIN8 X := X + 1;9 Y := Y * X10 END11 END;ENTRY: N ≥≥≥≥ 0 EXIT: Y = N! Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 21Procedures and Parameters:An Axiomatic Approach• Extended the axiomatic approach to procedures• Dealt explicitly with recursion“This assumption of what we want to prove before embarking on the proof explains well the aura of magic which attends a programmer’s first introduction to recursive programming”Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 22Rule of Recursive Invocationp(x):(v) proc Q, P{call p(x):(v)}R |- P{Q}RP{call p(x):(v)}R Hoare’s Axiiomatic SemanticsGCMPSC 266 Pg. 23An Axiomatic Definition of the Programming Language PASCALC.A.R. Hoare and N. WirthActa Informatica