Theory VcgExSP
section ‹Examples using Statespaces›
theory VcgExSP imports "../HeapList" "../Vcg" begin
subsection ‹State Spaces›
text ‹
First of all we provide a store of program variables that
occur in the programs considered later. Slightly unexpected
things may happen when attempting to work with undeclared variables.
›
hoarestate state_space =
A :: nat
I :: nat
M :: nat
N :: nat
R :: nat
S :: nat
B :: bool
Abr:: string
lemma (in state_space)"Γ⊢ ⦃´N = n⦄ LOC ´N :== 10;; ´N :== ´N + 2 COL ⦃´N = n⦄"
by vcg
text ‹Internally we decorate the state components in the statespace with the
suffix ‹_'›,
to avoid cluttering the namespace with the simple names that could no longer
be used for logical variables otherwise.
›
text ‹We will first consider programs without procedures, later on
we will regard procedures without global variables and finally we
will get the full pictures: mutually recursive procedures with global
variables (including heap).
›
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.
›
text ‹
Using the basic rule directly is a bit cumbersome.
›
lemma (in state_space) "Γ⊢ {|´N = 5|} ´N :== 2 * ´N {|´N = 10|}"
apply (rule HoarePartial.Basic)
apply simp
done
lemma (in state_space) "Γ⊢ ⦃True⦄ ´N :== 10 ⦃´N = 10⦄"
by vcg
lemma (in state_space) "Γ⊢ ⦃2 * ´N = 10⦄ ´N :== 2 * ´N ⦃´N = 10⦄"
by vcg
lemma (in state_space) "Γ⊢ ⦃´N = 5⦄ ´N :== 2 * ´N ⦃´N = 10⦄"
apply vcg
apply simp
done
lemma (in state_space) "Γ⊢ ⦃´N + 1 = a + 1⦄ ´N :== ´N + 1 ⦃´N = a + 1⦄"
by vcg
lemma (in state_space) "Γ⊢ ⦃´N = a⦄ ´N :== ´N + 1 ⦃´N = a + 1⦄"
apply vcg
apply simp
done
lemma (in state_space)
shows "Γ⊢ ⦃a = a ∧ b = b⦄ ´M :== a;; ´N :== b ⦃´M = a ∧ ´N = b⦄"
by vcg
lemma (in state_space)
shows "Γ⊢ ⦃True⦄ ´M :== a;; ´N :== b ⦃´M = a ∧ ´N = b⦄"
by vcg
lemma (in state_space)
shows "Γ⊢ ⦃´M = a ∧ ´N = b⦄
´I :== ´M;; ´M :== ´N;; ´N :== ´I
⦃´M = b ∧ ´N = a⦄"
apply vcg
apply simp
done
text ‹
We can also perform verification conditions generation step by step by using
the ‹vcg_step› method.
›
lemma (in state_space)
shows "Γ⊢ ⦃´M = a ∧ ´N = b⦄
´I :== ´M;; ´M :== ´N;; ´N :== ´I
⦃´M = b ∧ ´N = a⦄"
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply simp
done
text ‹
In the following assignments we make use of the consequence rule in
order to achieve the intended precondition. Certainly, the
‹vcg› method is able to handle this case, too.
›
lemma (in state_space)
shows "Γ⊢ ⦃´M = ´N⦄ ´M :== ´M + 1 ⦃´M ≠ ´N⦄"
proof -
have "⦃´M = ´N⦄ ⊆ ⦃´M + 1 ≠ ´N⦄"
by auto
also have "Γ⊢ … ´M :== ´M + 1 ⦃´M ≠ ´N⦄"
by vcg
finally show ?thesis .
qed
lemma (in state_space)
shows "Γ⊢ ⦃´M = ´N⦄ ´M :== ´M + 1 ⦃´M ≠ ´N⦄"
proof -
have "⋀m n::nat. m = n ⟶ m + 1 ≠ n"
by simp
also have "Γ⊢ ⦃´M + 1 ≠ ´N⦄ ´M :== ´M + 1 ⦃´M ≠ ´N⦄"
by vcg
finally show ?thesis .
qed
lemma (in state_space)
shows "Γ⊢ ⦃´M = ´N⦄ ´M :== ´M + 1 ⦃´M ≠ ´N⦄"
apply vcg
apply simp
done
subsection ‹Multiplication by Addition›
text ‹
We now do some basic examples of actual \texttt{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 (in state_space)
shows "Γ⊢ ⦃´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 vcg
finally show "Γ⊢ ⦃´?inv ∧ ´M ≠ a⦄ ?c ⦃´?inv⦄" .
qed
also have "⦃´?inv ∧ ¬ (´M ≠ a)⦄ ⊆ ⦃´S = a * b⦄" by auto
finally show ?thesis by blast
qed
text ‹
The subsequent version of the proof applies the ‹vcg› method
to reduce the Hoare statement to a purely logical problem that can be
solved fully automatically. Note that we have to specify the
\texttt{WHILE} loop invariant in the original statement.
›
lemma (in state_space)
shows "Γ⊢ ⦃´M = 0 ∧ ´S = 0⦄
WHILE ´M ≠ a
INV ⦃´S = ´M * b⦄
DO ´S :== ´S + b;; ´M :== ´M + 1 OD
⦃´S = a * b⦄"
apply vcg
apply auto
done
text ‹Here some examples of ``breaking'' out of a loop›
lemma (in state_space)
shows "Γ⊢ ⦃´M = 0 ∧ ´S = 0⦄
TRY
WHILE True
INV ⦃´S = ´M * b⦄
DO IF ´M = a THEN THROW ELSE ´S :== ´S + b;; ´M :== ´M + 1 FI OD
CATCH
SKIP
END
⦃´S = a * b⦄"
apply vcg
apply auto
done
lemma (in state_space)
shows "Γ⊢ ⦃´M = 0 ∧ ´S = 0⦄
TRY
WHILE True
INV ⦃´S = ´M * b⦄
DO IF ´M = a THEN ´Abr :== ''Break'';;THROW
ELSE ´S :== ´S + b;; ´M :== ´M + 1
FI
OD
CATCH
IF ´Abr = ''Break'' THEN SKIP ELSE Throw FI
END
⦃´S = a * b⦄"
apply vcg
apply auto
done
text ‹Some more syntactic sugar, the label statement ‹… ∙ …› as shorthand
for the ‹TRY-CATCH› above, and the ‹RAISE› for an state-update followed
by a ‹THROW›.
›
lemma (in state_space)
shows "Γ⊢ ⦃´M = 0 ∧ ´S = 0⦄
⦃´Abr = ''Break''⦄∙ WHILE True INV ⦃´S = ´M * b⦄
DO IF ´M = a THEN RAISE ´Abr :== ''Break''
ELSE ´S :== ´S + b;; ´M :== ´M + 1
FI
OD
⦃´S = a * b⦄"
apply vcg
apply auto
done
lemma (in state_space)
shows "Γ⊢ ⦃´M = 0 ∧ ´S = 0⦄
TRY
WHILE True
INV ⦃´S = ´M * b⦄
DO IF ´M = a THEN RAISE ´Abr :== ''Break''
ELSE ´S :== ´S + b;; ´M :== ´M + 1
FI
OD
CATCH
IF ´Abr = ''Break'' THEN SKIP ELSE Throw FI
END
⦃´S = a * b⦄"
apply vcg
apply auto
done
lemma (in state_space)
shows "Γ⊢ ⦃´M = 0 ∧ ´S = 0⦄
⦃´Abr = ''Break''⦄ ∙ WHILE True
INV ⦃´S = ´M * b⦄
DO IF ´M = a THEN RAISE ´Abr :== ''Break''
ELSE ´S :== ´S + b;; ´M :== ´M + 1
FI
OD
⦃´S = a * b⦄"
apply vcg
apply auto
done
text ‹Blocks›
lemma (in state_space)
shows "Γ⊢⦃´I = i⦄ LOC ´I;; ´I :== 2 COL ⦃´I ≤ i⦄"
apply vcg
by simp
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.
›
primrec
sum :: "(nat => nat) => nat => nat"
where
"sum f 0 = 0"
| "sum f (Suc n) = f n + sum f n"
syntax
"_sum" :: "idt => nat => nat => nat"
(‹SUMM _<_. _› [0, 0, 10] 10)
syntax_consts
"_sum" == sum
translations
"SUMM j<k. b" == "CONST sum (λj. b) k"
text ‹
The following proof is quite explicit in the individual steps taken,
with the ‹vcg› 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 (in state_space)
shows "Γ⊢ ⦃True⦄
´S :== 0;; ´I :== 1;;
WHILE ´I ≠ n
DO
´S :== ´S + ´I;;
´I :== ´I + 1
OD
⦃´S = (SUMM j<n. j)⦄"
(is "Γ⊢ _ (_;; ?while) _")
proof -
let ?sum = "λk. SUMM j<k. j"
let ?inv = "λs i. 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 vcg
finally show ?thesis .
qed
also have "Γ⊢ ⦃?inv ´S ´I⦄ ?while ⦃?inv ´S ´I ∧ ¬ ´I ≠ n⦄"
proof
let ?body = "´S :== ´S + ´I;; ´I :== ´I + 1"
have "⋀s i. ?inv s i ∧ i ≠ n ⟶ ?inv (s + i) (i + 1)"
by simp
also have "Γ⊢ ⦃´S + ´I = ?sum (´I + 1)⦄ ?body ⦃?inv ´S ´I⦄"
by vcg
finally show "Γ⊢ ⦃?inv ´S ´I ∧ ´I ≠ n⦄ ?body ⦃?inv ´S ´I⦄" .
qed
also have "⋀s i. s = ?sum i ∧ ¬ i ≠ n ⟶ s = ?sum n"
by simp
finally show ?thesis .
qed
text ‹
The next version uses the ‹vcg› method, while still explaining
the resulting proof obligations in an abstract, structured manner.
›
theorem (in state_space)
shows "Γ⊢ ⦃True⦄
´S :== 0;; ´I :== 1;;
WHILE ´I ≠ n
INV ⦃´S = (SUMM j<´I. j)⦄
DO
´S :== ´S + ´I;;
´I :== ´I + 1
OD
⦃´S = (SUMM j<n. j)⦄"
proof -
let ?sum = "λk. SUMM j<k. j"
let ?inv = "λs i. s = ?sum i"
show ?thesis
proof vcg
show "?inv 0 1" by simp
next
fix i s assume "?inv s i" "i ≠ n"
thus "?inv (s + i) (i + 1)" by simp
next
fix i s assume x: "?inv s i" "¬ i ≠ n"
thus "s = ?sum n" by simp
qed
qed
text ‹
Certainly, this proof may be done fully automatically as well, provided
that the invariant is given beforehand.
›
theorem (in state_space)
shows "Γ⊢ ⦃True⦄
´S :== 0;; ´I :== 1;;
WHILE ´I ≠ n
INV ⦃´S = (SUMM j<´I. j)⦄
DO
´S :== ´S + ´I;;
´I :== ´I + 1
OD
⦃´S = (SUMM j<n. j)⦄"
apply vcg
apply auto
done
subsection ‹SWITCH›
lemma (in state_space)
shows "Γ⊢ ⦃´N = 5⦄ SWITCH ´B
{True} ⇒ ´N :== 6
| {False} ⇒ ´N :== 7
END
⦃´N > 5⦄"
apply vcg
apply simp
done
lemma (in state_space)
shows "Γ⊢ ⦃´N = 5⦄ SWITCH ´N
{v. v < 5} ⇒ ´N :== 6
| {v. v ≥ 5} ⇒ ´N :== 7
END
⦃´N > 5⦄"
apply vcg
apply simp
done
subsection ‹(Mutually) Recursive Procedures›
subsubsection ‹Factorial›
text ‹We want to define a procedure for the factorial. We first
define a HOL functions that calculates it to specify the procedure later on.
›
primrec fac:: "nat ⇒ nat"
where
"fac 0 = 1" |
"fac (Suc n) = (Suc n) * fac n"
lemma fac_simp [simp]: "0 < i ⟹ fac i = i * fac (i - 1)"
by (cases i) simp_all
text ‹Now we define the procedure›
procedures
Fac (N::nat|R::nat)
"IF ´N = 0 THEN ´R :== 1
ELSE ´R :== CALL Fac(´N - 1);;
´R :== ´N * ´R
FI"
print_locale Fac_impl
text ‹
To see how a call is syntactically translated you can switch off the
printing translation via the configuration option ‹hoare_use_call_tr'›
›
context Fac_impl
begin
text ‹
@{term "CALL Fac(´N,´R)"} is internally:
›
declare [[hoare_use_call_tr' = false]]
text ‹
@{term "CALL Fac(´N,´R)"}
›
term "CALL Fac(´N,´R)"
declare [[hoare_use_call_tr' = true]]
text ‹
Now let us prove that @{term "Fac"} meets its specification.
›
end
lemma (in Fac_impl) Fac_spec':
shows "∀σ. Γ,Θ⊢{σ} PROC Fac(´N,´R) ⦃´R = fac ⇗σ⇖N⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply simp
done
text ‹
Since the factorial was implemented recursively,
the main ingredient of this proof is, to assume that the specification holds for
the recursive call of @{term Fac} and prove the body correct.
The assumption for recursive calls is added to the context by
the rule @{thm [source] HoarePartial.ProcRec1}
(also derived from general rule for mutually recursive procedures):
@{thm [display] HoarePartial.ProcRec1 [no_vars]}
The verification condition generator will infer the specification out of the
context when it encounters a recursive call of the factorial.
›
text ‹We can also step through verification condition generation. When
the verification condition generator encounters a procedure call it tries to
use the rule ‹ProcSpec›. To be successful there must be a specification
of the procedure in the context.
›
lemma (in Fac_impl) Fac_spec1:
shows "∀σ. Γ,Θ⊢{σ} ´R :== PROC Fac(´N) ⦃´R = fac ⇗σ⇖N⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply simp
done
text ‹Here some Isar style version of the proof›
lemma (in Fac_impl) Fac_spec2:
shows "∀σ. Γ,Θ⊢{σ} ´R :== PROC Fac(´N) ⦃´R = fac ⇗σ⇖N⦄"
proof (hoare_rule HoarePartial.ProcRec1)
have Fac_spec: "∀σ. Γ,(Θ∪(⋃σ. {({σ}, Fac_'proc, ⦃´R = fac ⇗σ⇖N⦄,{})}))
⊢ {σ} ´R :== PROC Fac(´N) ⦃´R = fac ⇗σ⇖N⦄"
apply (rule allI)
apply (rule hoarep.Asm)
by simp
show "∀σ. Γ,(Θ∪(⋃σ. {({σ}, Fac_'proc, ⦃´R = fac ⇗σ⇖N⦄,{})}))
⊢ {σ} IF ´N = 0 THEN ´R :== 1
ELSE ´R :== CALL Fac(´N - 1);; ´R :== ´N * ´R FI ⦃´R = fac ⇗σ⇖N⦄"
apply vcg
apply simp
done
qed
text ‹To avoid retyping of potentially large pre and postconditions in
the previous proof we can use the casual term abbreviations of the Isar
language.
›
lemma (in Fac_impl) Fac_spec3:
shows "∀σ. Γ,Θ⊢{σ} ´R :== PROC Fac(´N) ⦃´R = fac ⇗σ⇖N⦄"
(is "∀σ. Γ,Θ⊢(?Pre σ) ?Fac (?Post σ)")
proof (hoare_rule HoarePartial.ProcRec1)
have Fac_spec: "∀σ. Γ,(Θ∪(⋃σ. {(?Pre σ, Fac_'proc, ?Post σ,{})}))
⊢(?Pre σ) ?Fac (?Post σ)"
apply (rule allI)
apply (rule hoarep.Asm)
by simp
show "∀σ. Γ,(Θ∪(⋃σ. {(?Pre σ, Fac_'proc, ?Post σ,{})}))
⊢ (?Pre σ) IF ´N = 0 THEN ´R :== 1
ELSE ´R :== CALL Fac(´N - 1);; ´R :== ´N * ´R FI (?Post σ)"
apply vcg
apply simp
done
qed
text ‹The previous proof pattern has still some kind of inconvenience.
The augmented context is always printed in the proof state. That can
mess up the state, especially if we have large specifications. This may
be annoying if we want to develop single step or structured proofs. In this
case it can be a good idea to introduce a new variable for the augmented
context.
›
lemma (in Fac_impl) Fac_spec4:
shows "∀σ. Γ,Θ⊢{σ} ´R :== PROC Fac(´N) ⦃´R = fac ⇗σ⇖N⦄"
(is "∀σ. Γ,Θ⊢(?Pre σ) ?Fac (?Post σ)")
proof (hoare_rule HoarePartial.ProcRec1)
define Θ' where "Θ' = Θ ∪ (⋃σ. {(?Pre σ, Fac_'proc, ?Post σ,{})})"
have Fac_spec: "∀σ. Γ,Θ'⊢(?Pre σ) ?Fac (?Post σ)"
by (unfold Θ'_def, rule allI, rule hoarep.Asm) simp
txt ‹We have to name the fact ‹Fac_spec›, so that the vcg can
use the specification for the recursive call, since it cannot infer it
from the opaque @{term "Θ'"}.›
show "∀σ. Γ,Θ'⊢ (?Pre σ) IF ´N = 0 THEN ´R :== 1
ELSE ´R :== CALL Fac(´N - 1);; ´R :== ´N * ´R FI (?Post σ)"
apply vcg
apply simp
done
qed
text ‹There are different rules available to prove procedure calls,
depending on the kind of postcondition and whether or not the
procedure is recursive or even mutually recursive.
See for example @{thm [source] HoareTotal.ProcRec1},
@{thm [source] HoareTotal.ProcNoRec1}.
They are all derived from the most general rule
@{thm [source] HoareTotal.ProcRec}.
All of them have some side-conditions concerning the parameter
passing protocol and its relation to the pre and postcondition. They can be
solved in a uniform fashion. Thats why we have created the method
‹hoare_rule›, which behaves like the method ‹rule› but automatically
tries to solve the side-conditions.
›
subsubsection ‹Odd and Even›
text ‹Odd and even are defined mutually recursive here. In the
‹procedures› command we conjoin both definitions with ‹and›.
›
procedures
odd(N::nat | A::nat) "IF ´N=0 THEN ´A:==0
ELSE IF ´N=1 THEN CALL even (´N - 1,´A)
ELSE CALL odd (´N - 2,´A)
FI
FI"
and
even(N::nat | A::nat) "IF ´N=0 THEN ´A:==1
ELSE IF ´N=1 THEN CALL odd (´N - 1,´A)
ELSE CALL even (´N - 2,´A)
FI
FI"
print_theorems
print_locale! odd_even_clique
text ‹To prove the procedure calls to @{term "odd"} respectively
@{term "even"} correct we first derive a rule to justify that we
can assume both specifications to verify the bodies. This rule can
be derived from the general @{thm [source] HoareTotal.ProcRec} rule. An ML function will
do this work:
›
ML ‹ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2)›
lemma (in odd_even_clique)
shows odd_spec: "∀σ. Γ⊢{σ} ´A :== PROC odd(´N)
⦃(∃b. ⇗σ⇖N = 2 * b + ´A) ∧ ´A < 2 ⦄" (is ?P1)
and even_spec: "∀σ. Γ⊢{σ} ´A :== PROC even(´N)
⦃(∃b. ⇗σ⇖N + 1 = 2 * b + ´A) ∧ ´A < 2 ⦄" (is ?P2)
proof -
have "?P1 ∧ ?P2"
apply (hoare_rule ProcRec2)
apply vcg
apply clarsimp
apply (rule_tac x="b + 1" in exI)
apply arith
apply vcg
apply clarsimp
apply arith
done
thus "?P1" "?P2"
by iprover+
qed
subsection ‹Expressions With Side Effects›
lemma (in state_space) shows "Γ⊢ ⦃True⦄
´N ≫ n. ´N :== ´N + 1 ≫
´M ≫ m. ´M :== ´M + 1 ≫
´R :== n + m
⦃´R = ´N + ´M - 2⦄"
apply vcg
apply simp
done
lemma (in Fac_impl) shows
"Γ⊢ ⦃True⦄
CALL Fac(´N) ≫ n. CALL Fac(´N) ≫ m.
´R :== n + m
⦃´R = fac ´N + fac ´N⦄"
proof -
note Fac_spec = Fac_spec4
show ?thesis
apply vcg
done
qed
lemma (in Fac_impl) shows
"Γ⊢ ⦃True⦄
CALL Fac(´N) ≫ n. CALL Fac(n) ≫ m.
´R :== m
⦃´R = fac (fac ´N)⦄"
proof -
note Fac_spec = Fac_spec4
show ?thesis
apply vcg
done
qed
subsection ‹Global Variables and Heap›
text ‹
Now we will define and verify some procedures on heap-lists. We consider
list structures consisting of two fields, a content element @{term "cont"} and
a reference to the next list element @{term "next"}. We model this by the
following state space where every field has its own heap.
›
hoarestate globals_list =
"next" :: "ref ⇒ ref"
cont :: "ref ⇒ nat"
text ‹Updates to global components inside a procedure will
always be propagated to the caller. This is implicitly done by the
parameter passing syntax translations. The record containing the global variables must begin with the prefix "globals".
›
text ‹We will first define an append function on lists. It takes two
references as parameters. It appends the list referred to by the first
parameter with the list referred to by the second parameter, and returns
the result right into the first parameter.
›
procedures (imports globals_list)
append(p::ref,q::ref|p::ref)
"IF ´p=Null THEN ´p :== ´q ELSE ´p →´next:== CALL append(´p→´next,´q) FI"
declare [[hoare_use_call_tr' = false]]
context append_impl
begin
term "CALL append(´p,´q,´p→´next)"
end
declare [[hoare_use_call_tr' = true]]
text ‹Below we give two specifications this time..
The first one captures the functional behaviour and focuses on the
entities that are potentially modified by the procedure, the second one
is a pure frame condition.
The list in the modifies clause has to list all global state components that
may be changed by the procedure. Note that we know from the modifies clause
that the @{term cont} parts of the lists will not be changed. Also a small
side note on the syntax. We use ordinary brackets in the postcondition
of the modifies clause, and also the state components do not carry the
acute, because we explicitly note the state @{term t} here.
The functional specification now introduces two logical variables besides the
state space variable @{term "σ"}, namely @{term "Ps"} and @{term "Qs"}.
They are universally quantified and range over both the pre and the postcondition, so
that we are able to properly instantiate the specification
during the proofs. The syntax ‹⦃σ. …⦄› is a shorthand to fix the current
state: ‹{s. σ = s …}›.
›
lemma (in append_impl) append_spec:
shows "∀σ Ps Qs. Γ⊢
⦃σ. List ´p ´next Ps ∧ List ´q ´next Qs ∧ set Ps ∩ set Qs = {}⦄
´p :== PROC append(´p,´q)
⦃List ´p ´next (Ps@Qs) ∧ (∀x. x∉set Ps ⟶ ´next x = ⇗σ⇖next x)⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply fastforce
done
text ‹The modifies clause is equal to a proper record update specification
of the following form.
›
lemma (in append_impl) shows "{t. t may_only_modify_globals Z in [next]}
=
{t. ∃next. globals t=update id id next_' (K_statefun next) (globals Z)}"
apply (unfold mex_def meq_def)
apply simp
done
text ‹If the verification condition generator works on a procedure call
it checks whether it can find a modifies clause in the context. If one
is present the procedure call is simplified before the Hoare rule
@{thm [source] HoareTotal.ProcSpec} is applied. Simplification of the procedure call means,
that the ``copy back'' of the global components is simplified. Only those
components that occur in the modifies clause will actually be copied back.
This simplification is justified by the rule @{thm [source] HoareTotal.ProcModifyReturn}.
So after this simplification all global components that do not appear in
the modifies clause will be treated as local variables.
›
text ‹You can study the effect of the modifies clause on the following two
examples, where we want to prove that @{term "append"} does not change
the @{term "cont"} part of the heap.
›
lemma (in append_impl)
shows "Γ⊢ ⦃´p=Null ∧ ´cont=c⦄ ´p :== CALL append(´p,Null) ⦃´cont=c⦄"
apply vcg
oops
text ‹To prove the frame condition,
we have to tell the verification condition generator to use only the
modifies clauses and not to search for functional specifications by
the parameter ‹spec=modifies› It will also try to solve the
verification conditions automatically.
›
lemma (in append_impl) append_modifies:
shows
"∀σ. Γ⊢ {σ} ´p :== PROC append(´p,´q){t. t may_only_modify_globals σ in [next]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done
lemma (in append_impl)
shows "Γ⊢ ⦃´p=Null ∧ ´cont=c⦄ ´p→´next :== CALL append(´p,Null) ⦃´cont=c⦄"
apply vcg
apply simp
done
text ‹
Of course we could add the modifies clause to the functional specification as
well. But separating both has the advantage that we split up the verification
work. We can make use of the modifies clause before we apply the
functional specification in a fully automatic fashion.
›
text ‹To verify the body of @{term "append"} we do not need the modifies
clause, since the specification does not talk about @{term "cont"} at all, and
we don't access @{term "cont"} inside the body. This may be different for
more complex procedures.
›
text ‹
To prove that a procedure respects the modifies clause, we only need
the modifies clauses of the procedures called in the body. We do not need
the functional specifications. So we can always prove the modifies
clause without functional specifications, but me may need the modifies
clause to prove the functional specifications.
›
subsubsection ‹Insertion Sort›
primrec sorted:: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool"
where
"sorted le [] = True" |
"sorted le (x#xs) = ((∀y∈set xs. le x y) ∧ sorted le xs)"
procedures (imports globals_list)
insert(r::ref,p::ref | p::ref)
"IF ´r=Null THEN SKIP
ELSE IF ´p=Null THEN ´p :== ´r;; ´p→´next :== Null
ELSE IF ´r→´cont ≤ ´p→´cont
THEN ´r→´next :== ´p;; ´p:==´r
ELSE ´p→´next :== CALL insert(´r,´p→´next)
FI
FI
FI"
text ‹
In the postcondition of the functional specification there is a small but
important subtlety. Whenever we talk about the @{term "cont"} part we refer to
the one of the pre-state, even in the conclusion of the implication.
The reason is, that we have separated out, that @{term "cont"} is not modified
by the procedure, to the modifies clause. So whenever we talk about unmodified
parts in the postcondition we have to use the pre-state part, or explicitely
state an equality in the postcondition.
The reason is simple. If the postcondition would talk about ‹´cont›
instead of ‹⇗σ⇖cont›, we will get a new instance of ‹cont› during
verification and the postcondition would only state something about this
new instance. But as the verification condition generator will use the
modifies clause the caller of ‹insert› instead will still have the
old ‹cont› after the call. Thats the sense of the modifies clause.
So the caller and the specification will simply talk about two different things,
without being able to relate them (unless an explicit equality is added to
the specification).
›
lemma (in insert_impl) insert_modifies:
"∀σ. Γ⊢ {σ} ´p :== PROC insert(´r,´p){t. t may_only_modify_globals σ in [next]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done
lemma (in insert_impl) insert_spec:
"∀σ Ps . Γ⊢ ⦃σ. List ´p ´next Ps ∧ sorted (≤) (map ´cont Ps) ∧
´r ≠ Null ∧ ´r ∉ set Ps⦄
´p :== PROC insert(´r,´p)
⦃∃Qs. List ´p ´next Qs ∧ sorted (≤) (map ⇗σ⇖cont Qs) ∧
set Qs = insert ⇗σ⇖r (set Ps) ∧
(∀x. x ∉ set Qs ⟶ ´next x = ⇗σ⇖next x)⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply (intro conjI impI)
apply fastforce
apply fastforce
apply fastforce
apply (clarsimp)
apply force
done
procedures (imports globals_list)
insertSort(p::ref | p::ref)
where r::ref q::ref
in
"´r:==Null;;
WHILE (´p ≠ Null) DO
´q :== ´p;;
´p :== ´p→´next;;
´r :== CALL insert(´q,´r)
OD;;
´p:==´r"
print_locale insertSort_impl
lemma (in insertSort_impl) insertSort_modifies:
shows
"∀σ. Γ⊢ {σ} ´p :== PROC insertSort(´p)
{t. t may_only_modify_globals σ in [next]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done
text ‹Insertion sort is not implemented recursively here but with a while
loop. Note that the while loop is not annotated with an invariant in the
procedure definition. The invariant only comes into play during verification.
Therefore we will annotate the body during the proof with the
rule @{thm [source] HoareTotal.annotateI}.
›
lemma (in insertSort_impl) insertSort_body_spec:
shows "∀σ Ps. Γ,Θ⊢ ⦃σ. List ´p ´next Ps ⦄
´p :== PROC insertSort(´p)
⦃∃Qs. List ´p ´next Qs ∧ sorted (≤) (map ⇗σ⇖cont Qs) ∧
set Qs = set Ps⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply (hoare_rule anno=
"´r :== Null;;
WHILE ´p ≠ Null
INV ⦃∃Qs Rs. List ´p ´next Qs ∧ List ´r ´next Rs ∧
set Qs ∩ set Rs = {} ∧
sorted (≤) (map ´cont Rs) ∧ set Qs ∪ set Rs = set Ps ∧
´cont = ⇗σ⇖cont ⦄
DO ´q :== ´p;; ´p :== ´p→´next;; ´r :== CALL insert(´q,´r) OD;;
´p :== ´r" in HoarePartial.annotateI)
apply vcg
apply fastforce
prefer 2
apply fastforce
apply (clarsimp)
apply (rule_tac x=ps in exI)
apply (intro conjI)
apply (rule heap_eq_ListI1)
apply assumption
apply clarsimp
apply (subgoal_tac "x≠p ∧ x ∉ set Rs")
apply auto
done
subsubsection "Memory Allocation and Deallocation"
text ‹The basic idea of memory management is to keep a list of allocated
references in the state space. Allocation of a new reference adds a
new reference to the list deallocation removes a reference. Moreover
we keep a counter "free" for the free memory.
›
hoarestate globals_list_alloc =
alloc::"ref list"
free::nat
"next"::"ref ⇒ ref"
cont::"ref ⇒ nat"
hoarestate locals_list_alloc =
i::nat
first::ref
p::ref
q::ref
r::ref
root::ref
tmp::ref
locale list_alloc = globals_list_alloc + locals_list_alloc
definition "sz = (2::nat)"
lemma (in list_alloc)
shows
"Γ,Θ⊢ ⦃´i = 0 ∧ ´first = Null ∧ n*sz ≤ ´free⦄
WHILE ´i < n
INV ⦃∃Ps. List ´first ´next Ps ∧ length Ps = ´i ∧ ´i ≤ n ∧
set Ps ⊆ set ´alloc ∧ (n - ´i)*sz ≤ ´free⦄
DO
´p :== NEW sz [´cont:==0,´next:== Null];;
´p→´next :== ´first;;
´first :== ´p;;
´i :== ´i+ 1
OD
⦃∃Ps. List ´first ´next Ps ∧ length Ps = n ∧ set Ps ⊆ set ´alloc⦄"
apply (vcg)
apply simp
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule_tac x="new (set alloc)#Ps" in exI)
apply clarsimp
apply (rule conjI)
apply fastforce
apply (simp add: sz_def)
apply (simp add: sz_def)
apply fastforce
done
lemma (in list_alloc)
shows
"Γ⊢ ⦃´i = 0 ∧ ´first = Null ∧ n*sz ≤ ´free⦄
WHILE ´i < n
INV ⦃∃Ps. List ´first ´next Ps ∧ length Ps = ´i ∧ ´i ≤ n ∧
set Ps ⊆ set ´alloc ∧ (n - ´i)*sz ≤ ´free⦄
DO
´p :== NNEW sz [´cont:==0,´next:== Null];;
´p→´next :== ´first;;
´first :== ´p;;
´i :== ´i+ 1
OD
⦃∃Ps. List ´first ´next Ps ∧ length Ps = n ∧ set Ps ⊆ set ´alloc⦄"
apply (vcg)
apply simp
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule_tac x="new (set alloc)#Ps" in exI)
apply clarsimp
apply (rule conjI)
apply fastforce
apply (simp add: sz_def)
apply (simp add: sz_def)
apply fastforce
done
subsection ‹Fault Avoiding Semantics›
text ‹
If we want to ensure that no runtime errors occur we can insert guards into
the code. We will not be able to prove any nontrivial Hoare triple
about code with guards, if we cannot show that the guards will never fail.
A trivial Hoare triple is one with an empty precondtion.
›
lemma (in list_alloc) "Γ,Θ⊢ ⦃True⦄ ⦃´p≠Null⦄⟼ ´p→´next :== ´p ⦃True⦄"
apply vcg
oops
lemma (in list_alloc) "Γ,Θ⊢ {} ⦃´p≠Null⦄⟼ ´p→´next :== ´p ⦃True⦄"
apply vcg
done
text ‹Let us consider this small program that reverts a list. At
first without guards.
›
lemma (in list_alloc)
shows
"Γ,Θ⊢ ⦃List ´p ´next Ps ∧ List ´q ´next Qs ∧ set Ps ∩ set Qs = {} ∧
set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄
WHILE ´p ≠ Null
INV ⦃∃ps qs. List ´p ´next ps ∧ List ´q ´next qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs ∧
set ps ⊆ set ´alloc ∧ set qs ⊆ set ´alloc⦄
DO ´r :== ´p;;
´p :== ´p→ ´next;;
´r→´next :== ´q;;
´q :== ´r OD
⦃List ´q ´next (rev Ps @ Qs) ∧ set Ps⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄"
apply (vcg)
apply fastforce+
done
text ‹If we want to ensure that we do not dereference @{term "Null"} or
access unallocated memory, we have to add some guards.
›
lemma (in list_alloc)
shows
"Γ,Θ⊢ ⦃List ´p ´next Ps ∧ List ´q ´next Qs ∧ set Ps ∩ set Qs = {} ∧
set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄
WHILE ´p ≠ Null
INV ⦃∃ps qs. List ´p ´next ps ∧ List ´q ´next qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs ∧
set ps ⊆ set ´alloc ∧ set qs ⊆ set ´alloc⦄
DO ´r :== ´p;;
⦃´p≠Null ∧ ´p∈set ´alloc⦄⟼ ´p :== ´p→ ´next;;
⦃´r≠Null ∧ ´r∈set ´alloc⦄⟼ ´r→´next :== ´q;;
´q :== ´r OD
⦃List ´q ´next (rev Ps @ Qs) ∧ set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄"
apply (vcg)
apply fastforce+
done
text ‹We can also just prove that no faults will occur, by giving the
trivial postcondition.
›
lemma (in list_alloc) rev_noFault:
shows
"Γ,Θ⊢ ⦃List ´p ´next Ps ∧ List ´q ´next Qs ∧ set Ps ∩ set Qs = {} ∧
set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄
WHILE ´p ≠ Null
INV ⦃∃ps qs. List ´p ´next ps ∧ List ´q ´next qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs ∧
set ps ⊆ set ´alloc ∧ set qs ⊆ set ´alloc⦄
DO ´r :== ´p;;
⦃´p≠Null ∧ ´p∈set ´alloc⦄⟼ ´p :== ´p→ ´next;;
⦃´r≠Null ∧ ´r∈set ´alloc⦄⟼ ´r→´next :== ´q;;
´q :== ´r OD
UNIV,UNIV"
apply (vcg)
apply fastforce+
done
lemma (in list_alloc) rev_moduloGuards:
shows
"Γ,Θ⊢⇘/{True}⇙ ⦃List ´p ´next Ps ∧ List ´q ´next Qs ∧ set Ps ∩ set Qs = {} ∧
set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄
WHILE ´p ≠ Null
INV ⦃∃ps qs. List ´p ´next ps ∧ List ´q ´next qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs ∧
set ps ⊆ set ´alloc ∧ set qs ⊆ set ´alloc⦄
DO ´r :== ´p;;
⦃´p≠Null ∧ ´p∈set ´alloc⦄√ ⟼ ´p :== ´p→ ´next;;
⦃´r≠Null ∧ ´r∈set ´alloc⦄√ ⟼ ´r→´next :== ´q;;
´q :== ´r OD
⦃List ´q ´next (rev Ps @ Qs) ∧ set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄"
apply vcg
apply fastforce+
done
lemma CombineStrip':
assumes deriv: "Γ,Θ⊢⇘/F⇙ P c' Q,A"
assumes deriv_strip: "Γ,Θ⊢⇘/{}⇙ P c'' UNIV,UNIV"
assumes c'': "c''= mark_guards False (strip_guards (-F) c')"
assumes c: "c = mark_guards False c'"
shows "Γ,Θ⊢⇘/{}⇙ P c Q,A"
proof -
from deriv_strip [simplified c'']
have "Γ,Θ⊢ P (strip_guards (- F) c') UNIV,UNIV"
by (rule HoarePartialProps.MarkGuardsD)
with deriv
have "Γ,Θ⊢ P c' Q,A"
by (rule HoarePartialProps.CombineStrip)
hence "Γ,Θ⊢ P mark_guards False c' Q,A"
by (rule HoarePartialProps.MarkGuardsI)
thus ?thesis
by (simp add: c)
qed
text ‹We can then combine the prove that no fault will occur with the
functional prove of the programm without guards to get the full proove by
the rule @{thm HoarePartialProps.CombineStrip}
›
lemma (in list_alloc)
shows
"Γ,Θ⊢ ⦃List ´p ´next Ps ∧ List ´q ´next Qs ∧ set Ps ∩ set Qs = {} ∧
set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄
WHILE ´p ≠ Null
INV ⦃∃ps qs. List ´p ´next ps ∧ List ´q ´next qs ∧ set ps ∩ set qs = {} ∧
rev ps @ qs = rev Ps @ Qs ∧
set ps ⊆ set ´alloc ∧ set qs ⊆ set ´alloc⦄
DO ´r :== ´p;;
⦃´p≠Null ∧ ´p∈set ´alloc⦄⟼ ´p :== ´p→ ´next;;
⦃´r≠Null ∧ ´r∈set ´alloc⦄⟼ ´r→´next :== ´q;;
´q :== ´r OD
⦃List ´q ´next (rev Ps @ Qs) ∧ set Ps ⊆ set ´alloc ∧ set Qs ⊆ set ´alloc⦄"
apply (rule CombineStrip' [OF rev_moduloGuards rev_noFault])
apply simp
apply simp
done
text ‹In the previous example the effort to split up the prove did not
really pay off. But when we think of programs with a lot of guards and
complicated specifications it may be better to first focus on a prove without
the messy guards. Maybe it is possible to automate the no fault proofs so
that it suffices to focus on the stripped program.
›
context list_alloc
begin
text ‹
The purpose of guards is to watch for faults that can occur during
evaluation of expressions. In the example before we watched for null pointer
dereferencing or memory faults. We can also look for array index bounds or
division by zero. As the condition of a while loop is evaluated in each
iteration we cannot just add a guard before the while loop. Instead we need
a special guard for the condition.
Example: @{term "WHILE ⦃´p≠Null⦄⟼ ´p→´next≠Null DO SKIP OD"}
›
end
subsection ‹Cicular Lists›
definition
distPath :: "ref ⇒ (ref ⇒ ref) ⇒ ref ⇒ ref list ⇒ bool" where
"distPath x next y as = (Path x next y as ∧ distinct as)"
lemma neq_dP: "⟦p ≠ q; Path p h q Ps; distinct Ps⟧ ⟹
∃Qs. p≠Null ∧ Ps = p#Qs ∧ p ∉ set Qs"
by (cases Ps, auto)
lemma (in list_alloc) circular_list_rev_I:
"Γ,Θ⊢ ⦃´root = r ∧ distPath ´root ´next ´root (r#Ps)⦄
´p :== ´root;; ´q :== ´root→´next;;
WHILE ´q ≠ ´root
INV ⦃∃ ps qs. distPath ´p ´next ´root ps ∧ distPath ´q ´next ´root qs ∧
´root = r ∧ r≠Null ∧ r ∉ set Ps ∧ set ps ∩ set qs = {} ∧
Ps = (rev ps) @ qs ⦄
DO ´tmp :== ´q;; ´q :== ´q→´next;; ´tmp→´next :== ´p;; ´p:==´tmp OD;;
´root→´next :== ´p
⦃´root = r ∧ distPath ´root ´next ´root (r#rev Ps)⦄"
apply (simp only:distPath_def)
apply vcg
apply (rule_tac x="[]" in exI)
apply fastforce
apply clarsimp
apply (drule (2) neq_dP)
apply (rule_tac x="q # ps" in exI)
apply clarsimp
apply fastforce
done
lemma path_is_list:"⋀a next b. ⟦Path b next a Ps ; a ∉ set Ps; a≠Null⟧
⟹ List b (next(a := Null)) (Ps @ [a])"
apply (induct Ps)
apply (auto simp add:fun_upd_apply)
done
text ‹
The simple algorithm for acyclic list reversal, with modified
annotations, works for cyclic lists as well.:
›
lemma (in list_alloc) circular_list_rev_II:
"Γ,Θ⊢
⦃´p = r ∧ distPath ´p ´next ´p (r#Ps)⦄
´q:==Null;;
WHILE ´p ≠ Null
INV
⦃ ((´q = Null) ⟶ (∃ps. distPath ´p ´next r ps ∧ ps = r#Ps)) ∧
((´q ≠ Null) ⟶ (∃ps qs. distPath ´q ´next r qs ∧ List ´p ´next ps ∧
set ps ∩ set qs = {} ∧ rev qs @ ps = Ps@[r])) ∧
¬ (´p = Null ∧ ´q = Null ∧ r = Null )
⦄
DO
´tmp :== ´p;; ´p :== ´p→´next;; ´tmp→´next :== ´q;; ´q:==´tmp
OD
⦃´q = r ∧ distPath ´q ´next ´q (r # rev Ps)⦄"
apply (simp only:distPath_def)
apply vcg
apply clarsimp
apply clarsimp
apply (case_tac "(q = Null)")
apply (fastforce intro: path_is_list)
apply clarify
apply (rule_tac x="psa" in exI)
apply (rule_tac x=" p # qs" in exI)
apply force
apply fastforce
done
text‹Although the above algorithm is more succinct, its invariant
looks more involved. The reason for the case distinction on @{term q}
is due to the fact that during execution, the pointer variables can
point to either cyclic or acyclic structures.
›
text ‹
When working on lists, its sometimes better to remove
@{thm[source] fun_upd_apply} from the simpset, and instead include @{thm[source] fun_upd_same} and @{thm[source] fun_upd_other} to
the simpset
›
lemma (in state_space) "Γ⊢ {σ}
´I :== ´M;;
ANNO τ. ⦃τ. ´I = ⇗σ⇖M⦄
´M :== ´N;; ´N :== ´I
⦃´M = ⇗τ⇖N ∧ ´N = ⇗τ⇖I⦄
⦃´M = ⇗σ⇖N ∧ ´N = ⇗σ⇖M⦄"
apply vcg
apply auto
done
context state_space
begin
term "ANNO (τ,m,k). (⦃τ. ´M = m⦄) ´M :== ´N;; ´N :== ´I ⦃´M = ⇗ τ⇖N & ´N = ⇗τ⇖I⦄,{}"
end
lemma (in state_space) "Γ⊢ ({σ} ∩ ⦃´M = 0 ∧ ´S = 0⦄)
(ANNO τ. ({τ} ∩ ⦃´A=⇗σ⇖A ∧ ´I=⇗σ⇖I ∧ ´M=0 ∧ ´S=0⦄)
WHILE ´M ≠ ´A
INV ⦃´S = ´M * ´I ∧ ´A=⇗τ⇖A ∧ ´I=⇗τ⇖I⦄
DO ´S :== ´S + ´I;; ´M :== ´M + 1 OD
⦃´S = ⇗τ⇖A * ⇗τ⇖I⦄)
⦃´S = ⇗σ⇖A * ⇗σ⇖I⦄"
apply vcg_step
apply vcg_step
apply simp
apply vcg_step
apply vcg_step
apply simp
apply vcg
apply simp
apply simp
apply vcg_step
apply auto
done
text ‹Just some test on marked, guards›
lemma (in state_space) "Γ⊢⦃True⦄ WHILE ⦃P ´N ⦄√, ⦃Q ´M⦄#, ⦃R ´N⦄⟼ ´N < ´M
INV ⦃´N < 2⦄ DO
´N :== ´M
OD
⦃hard⦄"
apply vcg
oops
lemma (in state_space) "Γ⊢⇘/{True}⇙ ⦃True⦄ WHILE ⦃P ´N ⦄√, ⦃Q ´M⦄#, ⦃R ´N⦄⟼ ´N < ´M
INV ⦃´N < 2⦄ DO
´N :== ´M
OD
⦃hard⦄"
apply vcg
oops
end