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