CS611 Lecture 14 Axiomatics Semantics II and Hoare Logic 29 September 2006Lecturer: Dexter Kozen1 Axiomatic Semantics II1.1 RefinementFor nondeterministic programs S and T, we say that S refines T iff for any starting state, the set of p os siblefinal states of S is a (not necessarily strict) subset of the s et of possible final states of T.Consider for exampleS4= if x = 1 → y := 1 [] x 6= 1 → skip fiT4= if x = 1 → y := 1 [] x = 1 → y := 2 [] x 6= 1 → skip fiFor input state (x = a, y = b), the only possible final states of S are (x = 1, y = 1) if a = 1 and (x = a, y = b)if a 6= 1, whereas the possible final states of T are {(x = 1, y = 1), (x = 1, y = 2)} if a = 1 and just(x = a, y = b) if a 6= 1, therefore S refines T.The refinement relation is usually used only with programming languages with some form of nondeter-ministic choice as a relative measure of how nondeterministic a program is. A correctness specification mightbe written using nondeterministic choice, since often we may be happy with any one of a range of outcomes.Any deterministic program that refines the specification is considered correct.1.2 Weakest Liberal PreconditionsRecall that the weakest precondition of a program S and a postcondition ϕ is the weakest precondition thatguarantees that S halts and satisfies ϕ upon halting.The weakest liberal precondition (wlp) of a program S and a postcondition ϕ is the weakest preconditionthat guarantees that if S halts, then it satisties ϕ upon halting. The weakest liberal precondition of S andϕ is denoted wlp S ϕ.The difference between wp S ϕ and wlp S ϕ is that wp S ϕ implies that S terminates, whereas wlp S ϕdoes not. Since wlp S ϕ is weaker than wp S ϕ, it is presumably easier to establish.Recall that weakest preconditions of the do construct of GCL are not necessarily expressible in first-orderlogic. In fact, the same will be true of the weakest liberal preconditions. However, we may be able to findsome precondition that w ill be sufficient to establish correctness, even though that precondition may notnecessarily be the weakest. In other words, we will find ψ such that ψ ⇒ wlp S ϕ.Recall that if and do statements look likeif B1→ S1[] B2→ S2[] · · · [] Bn→ Snfido B1→ S1[] B2→ S2[] · · · [] Bn→ SnodDefineB4=n_i=1Bi.We will look for a property ψ such that(i) ψ ∧ B ⇒ wlp (if B1→ S1[] B2→ S2[] · · · [] Bn→ Snfi) ψ(ii) ψ ∧ ¬B ⇒ ϕ.Property (i) says that ψ is a loop invariant: if it holds before execution of the body of the do loop, and if atleast one clause in the body is enabled, then it holds after one execution of the body. It follows by induction1that if ψ holds before execution of the do loop, then it will hold after any number of iterations of the loop.Prop e rty (ii) says that if ψ holds and no clause of the loop is enabled (so that the loop will fall through),then the pos tcondition ϕ is satisfied.These observations say that the following proof rule is valid:ψ ∧ B ⇒ wlp (if B1→ S1[] B2→ S2[] · · · [] Bn→ Snfi) ψ ψ ∧ ¬B ⇒ ϕψ ⇒ wlp (do B1→ S1[] B2→ S2[] · · · [] Bn→ Sndo) ϕ.Note that a loop invariant need not hold continuously throughout the execution of the body of the loop.It is enough that it holds when the loop iteration is complete.For example, consider the following program, which for some function f : Int → Bool finds the least xsuch that f(x) (assume that such an x exists, so that the program will terminate).x := 0;do ¬f(x) → x := x + 1 odAn appropriate postcondition that specifies what it means for the program to be correct isϕ4⇐⇒ f(x) ∧ ∀y 0 ≤ y < x ⇒ ¬f(y).(read as “f holds of x and does not hold of any number smaller than x”). One method of finding a goodloop invariant is to look at ways of weakening the postcondition, thereby allowing more states to satisfy thepredicate. In this case, we can eliminate the conjunct asserting that we have already found a good x. Thisyields the invariantψ4⇐⇒ ∀y 0 ≤ y < x ⇒ ¬f(y).One can show that this is indeed an invariant and satisfies the two premises of the proof rule above withB = ¬f(x), thereforeψ ⇒ wlp (do ¬f(x) → x := x + 1 od) ϕ.The definitions of wlp S ϕ for the other basic constructs of GLC are the same as wp S ϕ except for if,which iswlp (if B1→ S1[] · · · [] Bn→ Snfi) ϕ4=n^i=1(Bi⇒ wlp Siϕ).Note that we no longer require B as with wp, since we do not have to ensure halting.2 Hoare LogicAs we have seen, calculating preconditions by hand is hard and not always tractable. We will now define alogic which allows us to reason about when assertions hold and therefore (hopefully) bypass most of thesekinds of computations.2.1 Partial vs. Total CorrectnessTwo approaches to program verification are:• Partial correctness: check if program is correct when it terminates. This is characterized by wlp andthe Hoare logic we will define shortly. The termination issue is handled separately.• Total correctness: ensure both that the program terminates and that it is correct. This is characterizedby wp.Partial correctness is the more common approach nowadays, since it separates the two issues of correctnessand termination. These two verification tasks use very different methods, and it is helpful to separate them.Often partial correctness is easier to establish, and once this is done, the correctness conditions can be usedin conjunction with a well-founded relation to establish termination.22.2 Syntax of Hoare LogicTo define Hoare logic, we need to define the well-formed formulas in the logic. Hoare logic is built on topof another conventional logic, such as first-order logic. For now, let us take first-order logic as our baselogic. Let ϕ, ψ, . . . denote first-order formulas. The formulas of Hoare logic are partial correctness assertions(PCA’s), also known as Hoare triples. They lo ok like{ϕ}S{ψ}.Informally, this means, “if ϕ holds before execution of S, and if S terminates, then ψ will hold upon termi-nation.” This is equivale nt toϕ ⇒ wlp S ψ.2.3 Proof RulesWe will discuss the semantics of Hoare logic later. For now, we just give the deduction rules for the languageIMP with programsc ::= skip | x := a | c0; c1| if b then c1else c2| while b do c.The rules are(skip) {ϕ}skip{ϕ}(assignment) {ϕ{a/x}}x := a{ϕ}(sequential composition){ϕ}c1{ψ} {ψ}c2{σ}{ϕ}c1; c2{σ}(conditional){b ∧ ϕ}c1{ψ} {¬b ∧ ϕ}c2{ψ}{ϕ}if b then c1else c2{ψ}(while){b