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 ‹_'›,
avoid cluttering the namespace with the simple names that could no longer
used for logical variables otherwise. ›
text‹We will first consider programs without procedures, later on
will regard procedures without global variables and finally we
get the full pictures: mutually recursive procedures with global
(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. ›
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 alsohave"Γ⊨…🍋M :== 🍋M + 1 {🍋M ≠🍋N}" by vcg finallyshow ?thesis . qed
lemma (in state_space) shows"Γ⊨{🍋M = 🍋N}🍋M :== 🍋M + 1 {🍋M ≠🍋N}" proof - have"∧m n::nat. m = n ⟶ m + 1 ≠ n"
― ‹inclusion of assertions expressed in ``pure'' logic,›
― ‹without mentioning the state space› by simp alsohave"Γ⊨{🍋M + 1 ≠🍋N}🍋M :== 🍋M + 1 {🍋M ≠🍋N}" by vcg finallyshow ?thesis . qed
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 alsohave"Γ⊨… ?while {🍋?inv ∧¬ (🍋M ≠ a)}" proof let ?c = "🍋S :== 🍋S + b;; 🍋M :== 🍋M + 1" have"{🍋?inv ∧🍋M ≠ a}⊆{🍋S + b = (🍋M + 1) * b}" by auto alsohave"Γ⊨… ?c {🍋?inv}"by vcg finallyshow"Γ⊨{🍋?inv ∧🍋M ≠ a} ?c {🍋?inv}" . qed alsohave"{🍋?inv ∧¬ (🍋M ≠ a)}⊆{🍋S = a * b}"by auto finallyshow ?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
the ‹TRY-CATCH› above, and the ‹RAISE› for an state-update followed
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"
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 alsohave"Γ⊨{…}🍋S :== 0;; 🍋I :== 1 {?inv 🍋S 🍋I}" by vcg finallyshow ?thesis . qed alsohave"Γ⊨{?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 alsohave"Γ⊨{🍋S + 🍋I = ?sum (🍋I + 1)} ?body {?inv 🍋S 🍋I}" by vcg finallyshow"Γ⊨{?inv 🍋S 🍋I ∧🍋I ≠ n} ?body {?inv 🍋S 🍋I}" . qed alsohave"∧s i. s = ?sum i ∧¬ i ≠ n ⟶ s = ?sum n" by simp finallyshow ?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
text‹
let us prove that @{term "Fac"} meets its specification. ›
end
lemma (in Fac_impl) Fac_spec': shows"∀σ. Γ,Θ⊨{σ} PROC Fac(🍋N,🍋R) {🍋R = fac <sigma>N}" apply (hoare_rule HoarePartial.ProcRec1) apply vcg apply simp done
text‹
the factorial was implemented recursively,
main ingredient of this proof is, to assume that the specification holds for
recursive call of @{term Fac} and prove the body correct.
assumption for recursive calls is added to the context by
rule @{thm [source] HoarePartial.ProcRec1}
also derived from general rule for mutually recursive procedures):
{thm [display] HoarePartial.ProcRec1 [no_vars]}
verification condition generator will infer the specification out of the
when it encounters a recursive call of the factorial. ›
text‹We can also step through verification condition generation. When
verification condition generator encounters a procedure call it tries to
use the rule ‹ProcSpec›. To be successful there must be a specification
the procedure in the context. ›
text‹The previous proof pattern has still some kind of inconvenience.
augmented context is always printed in the proof state. That can
up the state, especially if we have large specifications. This may
annoying if we want to develop single step or structured proofs. In this
it can be a good idea to introduce a new variable for the augmented
. ›
lemma (in Fac_impl) Fac_spec4: shows"∀σ. Γ,Θ⊨{σ} 🍋R :== PROC Fac(🍋N) {🍋R = fac <sigma>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,
on the kind of postcondition and whether or not the
is recursive or even mutually recursive.
for example @{thm [source] HoareTotal.ProcRec1},
{thm [source] HoareTotal.ProcNoRec1}.
are all derived from the most general rule
{thm [source] HoareTotal.ProcRec}.
of them have some side-conditions concerning the parameter
protocol and its relation to the pre and postcondition. They can be
in a uniform fashion. Thats why we have created the method ‹hoare_rule›, which behaves like the method ‹rule› but automatically
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
assume both specifications to verify the bodies. This rule can
derived from the general @{thm [source] HoareTotal.ProcRec} rule. An ML function will
this work: ›
ML ‹ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2)›
(* R := N++ + M++*) 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
(* R := Fac (N) + Fac (N) *) 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
(* R := Fac (N) + Fac (M) *) 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‹
we will define and verify some procedures on heap-lists. We consider
structures consisting of two fields, a content element @{term "cont"} and
reference to the next list element @{term "next"}. We model this by the
state space where every field has its own heap. ›
text‹Updates to global components inside a procedure will
be propagated to the caller. This is implicitly done by the
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
as parameters. It appends the list referred to by the first
with the list referred to by the second parameter, and returns
result right into the first parameter. ›
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..
first one captures the functional behaviour and focuses on the
that are potentially modified by the procedure, the second one
a pure frame condition.
list in the modifies clause has to list all global state components that
be changed by the procedure. Note that we know from the modifies clause
the @{term cont} parts of the lists will not be changed. Also a small
note on the syntax. We use ordinary brackets in the postcondition
the modifies clause, and also the state components do not carry the
, because we explicitly note the state @{term t} here.
functional specification now introduces two logical variables besides the
space variable @{term "σ"}, namely @{term "Ps"} and @{term "Qs"}.
are universally quantified and range over both the pre and the postcondition, so
we are able to properly instantiate the specification
the proofs. The syntax ‹{σ. …}› is a shorthand to fix the current
: ‹{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 = <sigma>next x)}" apply (hoare_rule HoarePartial.ProcRec1) apply vcg apply fastforce done
text‹The modifies clause is equal to a proper record update specification
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
checks whether it can find a modifies clause in the context. If one
present the procedure call is simplified before the Hoare rule
{thm [source] HoareTotal.ProcSpec} is applied. Simplification of the procedure call means,
the ``copy back'' of the global components is simplified. Only those
that occur in the modifies clause will actually be copied back.
simplification is justified by the rule @{thm [source] HoareTotal.ProcModifyReturn}.
after this simplification all global components that do not appear in
modifies clause will be treated as local variables. ›
text‹You can study the effect of the modifies clause on the following two
, where we want to prove that @{term "append"} does not change
@{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,
have to tell the verification condition generator to use only the
clauses and not to search for functional specifications by
parameter ‹spec=modifies› It will also try to solve the
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
text‹
course we could add the modifies clause to the functional specification as
. But separating both has the advantage that we split up the verification
. We can make use of the modifies clause before we apply the
specification in a fully automatic fashion. ›
text‹To verify the body of @{term "append"} we do not need the modifies
, since the specification does not talk about @{term "cont"} at all, and
don't access @{term "cont"} inside the body. This may be different for
complex procedures. ›
text‹
prove that a procedure respects the modifies clause, we only need
modifies clauses of the procedures called in the body. We do not need
functional specifications. So we can always prove the modifies
without functional specifications, but me may need the modifies
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‹
the postcondition of the functional specification there is a small but
subtlety. Whenever we talk about the @{term "cont"} part we refer to
one of the pre-state, even in the conclusion of the implication.
reason is, that we have separated out, that @{term "cont"} is not modified
the procedure, to the modifies clause. So whenever we talk about unmodified
in the postcondition we have to use the pre-state part, or explicitely
an equality in the postcondition.
reason is simple. If the postcondition would talk about ‹🍋cont›
of ‹σcont›, we will get a new instance of ‹cont› during
and the postcondition would only state something about this
instance. But as the verification condition generator will use the
clause the caller of ‹insert› instead will still have the ‹cont› after the call. Thats the sense of the modifies clause.
the caller and the specification will simply talk about two different things,
being able to relate them (unless an explicit equality is added to
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 <sigma>cont Qs) ∧ set Qs = insert <sigma>r (set Ps) ∧ (∀x. x ∉ set Qs ⟶🍋next x = <sigma>next x)}"
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
. Note that the while loop is not annotated with an invariant in the
definition. The invariant only comes into play during verification.
we will annotate the body during the proof with the
@{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 <sigma>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 = <sigma>cont } DO 🍋q :== 🍋p;; 🍋p :== 🍋p→🍋next;; 🍋r :== CALL insert(🍋q,🍋r) OD;; 🍋p :== 🍋r"in HoarePartial.annotateI) apply vcg apply fastforce prefer2 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
in the state space. Allocation of a new reference adds a
reference to the list deallocation removes a reference. Moreover
keep a counter "free" for the free memory. ›
text‹
we want to ensure that no runtime errors occur we can insert guards into
code. We will not be able to prove any nontrivial Hoare triple
code with guards, if we cannot show that the guards will never fail.
trivial Hoare triple is one with an empty precondtion. ›
lemma (in list_alloc) "Γ,Θ⊨{True}{🍋p≠Null}⟼🍋p→🍋next :== 🍋p {True}" apply vcg oops
text‹Let us consider this small program that reverts a list. At
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
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
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
prove of the programm without guards to get the full proove by
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}"
text‹In the previous example the effort to split up the prove did not
pay off. But when we think of programs with a lot of guards and
specifications it may be better to first focus on a prove without
messy guards. Maybe it is possible to automate the no fault proofs so
it suffices to focus on the stripped program. ›
context list_alloc begin text‹
purpose of guards is to watch for faults that can occur during
of expressions. In the example before we watched for null pointer
or memory faults. We can also look for array index bounds or
by zero. As the condition of a while loop is evaluated in each
we cannot just add a guard before the while loop. Instead we need
special guard for the condition.
: @{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 path_is_list:"∧a next b. [Path b next a Ps ; a ∉ set Ps; a≠Null] \<Longrightarrow> List b (next(a := Null)) (Ps @ [a])" apply (induct Ps) apply (auto simp add:fun_upd_apply) done
text‹
simple algorithm for acyclic list reversal, with modified
, works for cyclic lists as well.: ›
lemma (in list_alloc) circular_list_rev_II: "Γ,Θ⊨ {🍋p = r ∧ distPath 🍋p 🍋next 🍋p (r#Ps)} \<acute>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)}"
text‹Although the above algorithm is more succinct, its invariant
more involved. The reason for the case distinction on @{term q}
due to the fact that during execution, the pointer variables can
to either cyclic or acyclic structures. ›
text‹
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
simpset ›
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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.40 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
