section ‹Using Hoare Logic› theory Hoare_Ex imports Hoare begin subsection ‹State spaces› text ‹ First of all we provide a store of program variables that occur in any of the programs considered later. Slightly unexpected things may happen when attempting to work with undeclared variables. › record vars = I :: nat M :: nat N :: nat S :: nat text ‹ While all of our variables happen to have the same type, nothing would prevent us from working with many-sorted programs as well, or even polymorphic ones. Also note that Isabelle/HOL's extensible record types even provides simple means to extend the state space later. › subsection ‹Basic examples› text ‹ We look at few trivialities involving assignment and sequential composition, in order to get an idea of how to work with our formulation of Hoare Logic. ┉ Using the basic ‹assign› rule directly is a bit cumbersome. › lemma "⊢ ⦃´(N_update (λ_. (2 * ´N))) ∈ ⦃´N = 10⦄⦄ ´N := 2 * ´N ⦃´N = 10⦄" by (rule assign) text ‹ Certainly we want the state modification already done, e.g.\ by simplification. The ‹hoare› method performs the basic state update for us; we may apply the Simplifier afterwards to achieve ``obvious'' consequences as well. › lemma "⊢ ⦃True⦄ ´N := 10 ⦃´N = 10⦄" by hoare lemma "⊢ ⦃2 * ´N = 10⦄ ´N := 2 * ´N ⦃´N = 10⦄" by hoare lemma "⊢ ⦃´N = 5⦄ ´N := 2 * ´N ⦃´N = 10⦄" by hoare simp lemma "⊢ ⦃´N + 1 = a + 1⦄ ´N := ´N + 1 ⦃´N = a + 1⦄" by hoare lemma "⊢ ⦃´N = a⦄ ´N := ´N + 1 ⦃´N = a + 1⦄" by hoare simp lemma "⊢ ⦃a = a ∧ b = b⦄ ´M := a; ´N := b ⦃´M = a ∧ ´N = b⦄" by hoare lemma "⊢ ⦃True⦄ ´M := a; ´N := b ⦃´M = a ∧ ´N = b⦄" by hoare lemma "⊢ ⦃´M = a ∧ ´N = b⦄ ´I := ´M; ´M := ´N; ´N := ´I ⦃´M = b ∧ ´N = a⦄" by hoare simp text ‹ It is important to note that statements like the following one can only be proven for each individual program variable. Due to the extra-logical nature of record fields, we cannot formulate a theorem relating record selectors and updates schematically. › lemma "⊢ ⦃´N = a⦄ ´N := ´N ⦃´N = a⦄" by hoare lemma "⊢ ⦃´x = a⦄ ´x := ´x ⦃´x = a⦄" oops lemma "Valid {s. x s = a} (Basic (λs. x_update (x s) s)) {s. x s = n}" ― ‹same statement without concrete syntax› oops text ‹ In the following assignments we make use of the consequence rule in order to achieve the intended precondition. Certainly, the ‹hoare› method is able to handle this case, too. › lemma "⊢ ⦃´M = ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄" proof - have "⦃´M = ´N⦄ ⊆ ⦃´M + 1 ≠ ´N⦄" by auto also have "⊢ … ´M := ´M + 1 ⦃´M ≠ ´N⦄" by hoare finally show ?thesis . qed lemma "⊢ ⦃´M = ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄" proof - have "m = n ⟶ m + 1 ≠ n" for m n :: nat ― ‹inclusion of assertions expressed in ``pure'' logic,› ― ‹without mentioning the state space› by simp also have "⊢ ⦃´M + 1 ≠ ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄" by hoare finally show ?thesis . qed lemma "⊢ ⦃´M = ´N⦄ ´M := ´M + 1 ⦃´M ≠ ´N⦄" by hoare simp subsection ‹Multiplication by addition› text ‹ We now do some basic examples of actual ▩‹WHILE› programs. This one is a loop for calculating the product of two natural numbers, by iterated addition. We first give detailed structured proof based on single-step Hoare rules. › lemma "⊢ ⦃´M = 0 ∧ ´S = 0⦄ WHILE ´M ≠ a DO ´S := ´S + b; ´M := ´M + 1 OD ⦃´S = a * b⦄" proof - let "⊢ _ ?while _" = ?thesis let "⦃´?inv⦄" = "⦃´S = ´M * b⦄" have "⦃´M = 0 ∧ ´S = 0⦄ ⊆ ⦃´?inv⦄" by auto also have "⊢ … ?while ⦃´?inv ∧ ¬ (´M ≠ a)⦄" proof let ?c = "´S := ´S + b; ´M := ´M + 1" have "⦃´?inv ∧ ´M ≠ a⦄ ⊆ ⦃´S + b = (´M + 1) * b⦄" by auto also have "⊢ … ?c ⦃´?inv⦄" by hoare finally show "⊢ ⦃´?inv ∧ ´M ≠ a⦄ ?c ⦃´?inv⦄" . qed also have "… ⊆ ⦃´S = a * b⦄" by auto finally show ?thesis . qed text ‹ The subsequent version of the proof applies the ‹hoare› method to reduce the Hoare statement to a purely logical problem that can be solved fully automatically. Note that we have to specify the ▩‹WHILE› loop invariant in the original statement. › lemma "⊢ ⦃´M = 0 ∧ ´S = 0⦄ WHILE ´M ≠ a INV ⦃´S = ´M * b⦄ DO ´S := ´S + b; ´M := ´M + 1 OD ⦃´S = a * b⦄" by hoare auto subsection ‹Summing natural numbers› text ‹ We verify an imperative program to sum natural numbers up to a given limit. First some functional definition for proper specification of the problem. ┉ The following proof is quite explicit in the individual steps taken, with the ‹hoare› method only applied locally to take care of assignment and sequential composition. Note that we express intermediate proof obligation in pure logic, without referring to the state space. › theorem "⊢ ⦃True⦄ ´S := 0; ´I := 1; WHILE ´I ≠ n DO ´S := ´S + ´I; ´I := ´I + 1 OD ⦃´S = (∑j<n. j)⦄" (is "⊢ _ (_; ?while) _") proof - let ?sum = "λk::nat. ∑j<k. j" let ?inv = "λs i::nat. s = ?sum i" have "⊢ ⦃True⦄ ´S := 0; ´I := 1 ⦃?inv ´S ´I⦄" proof - have "True ⟶ 0 = ?sum 1" by simp also have "⊢ ⦃…⦄ ´S := 0; ´I := 1 ⦃?inv ´S ´I⦄" by hoare finally show ?thesis . qed also have "⊢ … ?while ⦃?inv ´S ´I ∧ ¬ ´I ≠ n⦄" proof let ?body = "´S := ´S + ´I; ´I := ´I + 1" have "?inv s i ∧ i ≠ n ⟶ ?inv (s + i) (i + 1)" for s i by simp also have "⊢ ⦃´S + ´I = ?sum (´I + 1)⦄ ?body ⦃?inv ´S ´I⦄" by hoare finally show "⊢ ⦃?inv ´S ´I ∧ ´I ≠ n⦄ ?body ⦃?inv ´S ´I⦄" . qed also have "s = ?sum i ∧ ¬ i ≠ n ⟶ s = ?sum n" for s i by simp finally show ?thesis . qed text ‹ The next version uses the ‹hoare› method, while still explaining the resulting proof obligations in an abstract, structured manner. › theorem "⊢ ⦃True⦄ ´S := 0; ´I := 1; WHILE ´I ≠ n INV ⦃´S = (∑j<´I. j)⦄ DO ´S := ´S + ´I; ´I := ´I + 1 OD ⦃´S = (∑j<n. j)⦄" proof - let ?sum = "λk::nat. ∑j<k. j" let ?inv = "λs i::nat. s = ?sum i" show ?thesis proof hoare show "?inv 0 1" by simp show "?inv (s + i) (i + 1)" if "?inv s i ∧ i ≠ n" for s i using that by simp show "s = ?sum n" if "?inv s i ∧ ¬ i ≠ n" for s i using that by simp qed qed text ‹ Certainly, this proof may be done fully automatic as well, provided that the invariant is given beforehand. › theorem "⊢ ⦃True⦄ ´S := 0; ´I := 1; WHILE ´I ≠ n INV ⦃´S = (∑j<´I. j)⦄ DO ´S := ´S + ´I; ´I := ´I + 1 OD ⦃´S = (∑j<n. j)⦄" by hoare auto subsection ‹Time› text ‹ A simple embedding of time in Hoare logic: function ‹timeit› inserts an extra variable to keep track of the elapsed time. › record tstate = time :: nat type_synonym 'a time = "⦇time :: nat, … :: 'a⦈" primrec timeit :: "'a time com ⇒ 'a time com" where "timeit (Basic f) = (Basic f; Basic(λs. s⦇time := Suc (time s)⦈))" | "timeit (c1; c2) = (timeit c1; timeit c2)" | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)" | "timeit (While b iv c) = While b iv (timeit c)" record tvars = tstate + I :: nat J :: nat lemma lem: "(0::nat) < n ⟹ n + n ≤ Suc (n * n)" by (induct n) simp_all lemma "⊢ ⦃i = ´I ∧ ´time = 0⦄ (timeit (WHILE ´I ≠ 0 INV ⦃2 *´ time + ´I * ´I + 5 * ´I = i * i + 5 * i⦄ DO ´J := ´I; WHILE ´J ≠ 0 INV ⦃0 < ´I ∧ 2 * ´time + ´I * ´I + 3 * ´I + 2 * ´J - 2 = i * i + 5 * i⦄ DO ´J := ´J - 1 OD; ´I := ´I - 1 OD)) ⦃2 * ´time = i * i + 5 * i⦄" apply simp apply hoare apply simp apply clarsimp apply clarsimp apply arith prefer 2 apply clarsimp apply (clarsimp simp: nat_distrib) apply (frule lem) apply arith done end