|
13875
|
1 |
(* Title: HOL/Hoare/Pointer_ExamplesAbort.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 2002 TUM
|
|
|
5 |
|
|
|
6 |
Examples of verifications of pointer programs
|
|
|
7 |
*)
|
|
|
8 |
|
|
16417
|
9 |
theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
|
|
13875
|
10 |
|
|
|
11 |
section "Verifications"
|
|
|
12 |
|
|
|
13 |
subsection "List reversal"
|
|
|
14 |
|
|
|
15 |
text "Interestingly, this proof is the same as for the unguarded program:"
|
|
|
16 |
|
|
|
17 |
lemma "VARS tl p q r
|
|
|
18 |
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
|
|
|
19 |
WHILE p \<noteq> Null
|
|
|
20 |
INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
|
|
|
21 |
rev ps @ qs = rev Ps @ Qs}
|
|
|
22 |
DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
|
|
|
23 |
{List tl q (rev Ps @ Qs)}"
|
|
|
24 |
apply vcg_simp
|
|
|
25 |
apply fastsimp
|
|
|
26 |
apply(fastsimp intro:notin_List_update[THEN iffD2])
|
|
|
27 |
apply fastsimp
|
|
|
28 |
done
|
|
|
29 |
|
|
|
30 |
end
|