# Theory Hoare_Ex

```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
›

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

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 v c) = While b iv v (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
```