src/HOL/Hoare/Pointer_Examples.thy
author nipkow
Sun Mar 23 11:57:07 2003 +0100 (2003-03-23)
changeset 13875 12997e3ddd8d
parent 13773 58dc4ab362d0
child 14062 7f0d5cc52615
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/Hoare/Pointers.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2002 TUM
     5 
     6 Examples of verifications of pointer programs
     7 *)
     8 
     9 theory Pointer_Examples = HeapSyntax:
    10 
    11 section "Verifications"
    12 
    13 subsection "List reversal"
    14 
    15 text "A short but unreadable proof:"
    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 := 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 (* explicit:
    28  apply clarify
    29  apply(rename_tac ps b qs)
    30  apply clarsimp
    31  apply(rename_tac ps')
    32  apply(fastsimp intro:notin_List_update[THEN iffD2])
    33  apply(rule_tac x = ps' in exI)
    34  apply simp
    35  apply(rule_tac x = "b#qs" in exI)
    36  apply simp
    37 *)
    38 apply fastsimp
    39 done
    40 
    41 
    42 text "A longer readable version:"
    43 
    44 lemma "VARS tl p q r
    45   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    46   WHILE p \<noteq> Null
    47   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    48                rev ps @ qs = rev Ps @ Qs}
    49   DO r := p; p := p^.tl; r^.tl := q; q := r OD
    50   {List tl q (rev Ps @ Qs)}"
    51 proof vcg
    52   fix tl p q r
    53   assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
    54   thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    55                 rev ps @ qs = rev Ps @ Qs" by fastsimp
    56 next
    57   fix tl p q r
    58   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    59                    rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
    60          (is "(\<exists>ps qs. ?I ps qs) \<and> _")
    61   then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
    62     by fast
    63   then obtain ps' where "ps = a # ps'" by fastsimp
    64   hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    65          List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
    66          set ps' \<inter> set (a#qs) = {} \<and>
    67          rev ps' @ (a#qs) = rev Ps @ Qs"
    68     using I by fastsimp
    69   thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    70                   List (tl(p \<rightarrow> q)) p       qs' \<and>
    71                   set ps' \<inter> set qs' = {} \<and>
    72                   rev ps' @ qs' = rev Ps @ Qs" by fast
    73 next
    74   fix tl p q r
    75   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    76                    rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
    77   thus "List tl q (rev Ps @ Qs)" by fastsimp
    78 qed
    79 
    80 
    81 text{* Finaly, the functional version. A bit more verbose, but automatic! *}
    82 
    83 lemma "VARS tl p q r
    84   {islist tl p \<and> islist tl q \<and>
    85    Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
    86   WHILE p \<noteq> Null
    87   INV {islist tl p \<and> islist tl q \<and>
    88        set(list tl p) \<inter> set(list tl q) = {} \<and>
    89        rev(list tl p) @ (list tl q) = rev Ps @ Qs}
    90   DO r := p; p := p^.tl; r^.tl := q; q := r OD
    91   {islist tl q \<and> list tl q = rev Ps @ Qs}"
    92 apply vcg_simp
    93   apply clarsimp
    94  apply clarsimp
    95 apply clarsimp
    96 done
    97 
    98 
    99 subsection "Searching in a list"
   100 
   101 text{*What follows is a sequence of successively more intelligent proofs that
   102 a simple loop finds an element in a linked list.
   103 
   104 We start with a proof based on the @{term List} predicate. This means it only
   105 works for acyclic lists. *}
   106 
   107 lemma "VARS tl p
   108   {List tl p Ps \<and> X \<in> set Ps}
   109   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   110   INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
   111   DO p := p^.tl OD
   112   {p = Ref X}"
   113 apply vcg_simp
   114   apply blast
   115  apply clarsimp
   116 apply clarsimp
   117 done
   118 
   119 text{*Using @{term Path} instead of @{term List} generalizes the correctness
   120 statement to cyclic lists as well: *}
   121 
   122 lemma "VARS tl p
   123   {Path tl p Ps X}
   124   WHILE p \<noteq> Null \<and> p \<noteq> X
   125   INV {\<exists>ps. Path tl p ps X}
   126   DO p := p^.tl OD
   127   {p = X}"
   128 apply vcg_simp
   129   apply blast
   130  apply fastsimp
   131 apply clarsimp
   132 done
   133 
   134 text{*Now it dawns on us that we do not need the list witness at all --- it
   135 suffices to talk about reachability, i.e.\ we can use relations directly. The
   136 first version uses a relation on @{typ"'a ref"}: *}
   137 
   138 lemma "VARS tl p
   139   {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   140   WHILE p \<noteq> Null \<and> p \<noteq> X
   141   INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   142   DO p := p^.tl OD
   143   {p = X}"
   144 apply vcg_simp
   145  apply clarsimp
   146  apply(erule converse_rtranclE)
   147   apply simp
   148  apply(clarsimp elim:converse_rtranclE)
   149 apply(fast elim:converse_rtranclE)
   150 done
   151 
   152 text{*Finally, a version based on a relation on type @{typ 'a}:*}
   153 
   154 lemma "VARS tl p
   155   {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   156   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   157   INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   158   DO p := p^.tl OD
   159   {p = Ref X}"
   160 apply vcg_simp
   161  apply clarsimp
   162  apply(erule converse_rtranclE)
   163   apply simp
   164  apply clarsimp
   165 apply clarsimp
   166 done
   167 
   168 
   169 subsection "Merging two lists"
   170 
   171 text"This is still a bit rough, especially the proof."
   172 
   173 constdefs
   174  cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   175 "cor P Q == if P then True else Q"
   176  cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   177 "cand P Q == if P then Q else False"
   178 
   179 consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
   180 
   181 recdef merge "measure(%(xs,ys,f). size xs + size ys)"
   182 "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
   183                                 else y # merge(x#xs,ys,f))"
   184 "merge(x#xs,[],f) = x # merge(xs,[],f)"
   185 "merge([],y#ys,f) = y # merge([],ys,f)"
   186 "merge([],[],f) = []"
   187 
   188 text{* Simplifies the proof a little: *}
   189 
   190 lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
   191 by blast
   192 lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
   193 by blast
   194 lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)"
   195 by blast
   196 
   197 lemma "VARS hd tl p q r s
   198  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   199   (p \<noteq> Null \<or> q \<noteq> Null)}
   200  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   201  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   202  s := r;
   203  WHILE p \<noteq> Null \<or> q \<noteq> Null
   204  INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
   205       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   206       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   207       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   208       (tl a = p \<or> tl a = q)}
   209  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   210     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   211     s := s^.tl
   212  OD
   213  {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   214 apply vcg_simp
   215 apply (simp_all add: cand_def cor_def)
   216 
   217 apply (fastsimp)
   218 
   219 apply clarsimp
   220 apply(rule conjI)
   221 apply clarsimp
   222 apply(rule conjI)
   223 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   224 apply clarsimp
   225 apply(rule conjI)
   226 apply (clarsimp)
   227 apply(rule_tac x = "rs @ [a]" in exI)
   228 apply(clarsimp simp:eq_sym_conv)
   229 apply(rule_tac x = "bs" in exI)
   230 apply(clarsimp simp:eq_sym_conv)
   231 apply(rule_tac x = "ya#bsa" in exI)
   232 apply(simp)
   233 apply(clarsimp simp:eq_sym_conv)
   234 apply(rule_tac x = "rs @ [a]" in exI)
   235 apply(clarsimp simp:eq_sym_conv)
   236 apply(rule_tac x = "y#bs" in exI)
   237 apply(clarsimp simp:eq_sym_conv)
   238 apply(rule_tac x = "bsa" in exI)
   239 apply(simp)
   240 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   241 
   242 apply(clarsimp simp add:List_app)
   243 done
   244 
   245 
   246 text{* More of the proof can be automated, but the runtime goes up
   247 drastically. In general it is usually more efficient to give the
   248 witness directly than to have it found by proof.
   249 
   250 Now we try a functional version of the abstraction relation @{term
   251 Path}. Since the result is not that convincing, we do not prove any of
   252 the lemmas.*}
   253 
   254 consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
   255        path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
   256 
   257 ML"set quick_and_dirty"
   258 
   259 text"First some basic lemmas:"
   260 
   261 lemma [simp]: "ispath f p p"
   262 sorry
   263 lemma [simp]: "path f p p = []"
   264 sorry
   265 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
   266 sorry
   267 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
   268  path (f(a := r)) p q = path f p q"
   269 sorry
   270 
   271 text"Some more specific lemmas needed by the example:"
   272 
   273 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
   274 sorry
   275 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
   276  path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
   277 sorry
   278 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
   279  b \<notin> set (path f p (Ref a))"
   280 sorry
   281 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
   282 sorry
   283 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
   284 sorry
   285 
   286 lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
   287 sorry
   288 ML"reset quick_and_dirty"
   289 
   290 lemma "VARS hd tl p q r s
   291  {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>
   292   set Ps \<inter> set Qs = {} \<and>
   293   (p \<noteq> Null \<or> q \<noteq> Null)}
   294  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   295  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   296  s := r;
   297  WHILE p \<noteq> Null \<or> q \<noteq> Null
   298  INV {EX rs ps qs a. ispath tl r s & rs = path tl r s \<and>
   299       islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<and>
   300       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   301       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   302       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   303       (tl a = p \<or> tl a = q)}
   304  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   305     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   306     s := s^.tl
   307  OD
   308  {islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   309 apply vcg_simp
   310 
   311 apply (simp_all add: cand_def cor_def)
   312   apply (fastsimp)
   313  apply (fastsimp simp: eq_sym_conv)
   314 apply(clarsimp)
   315 done
   316 
   317 text"The proof is automatic, but requires a numbet of special lemmas."
   318 
   319 
   320 subsection "Storage allocation"
   321 
   322 constdefs new :: "'a set \<Rightarrow> 'a"
   323 "new A == SOME a. a \<notin> A"
   324 
   325 
   326 lemma new_notin:
   327  "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
   328 apply(unfold new_def)
   329 apply(rule someI2_ex)
   330  apply (fast intro:ex_new_if_finite)
   331 apply (fast)
   332 done
   333 
   334 
   335 lemma "~finite(UNIV::'a set) \<Longrightarrow>
   336   VARS xs elem next alloc p q
   337   {Xs = xs \<and> p = (Null::'a ref)}
   338   WHILE xs \<noteq> []
   339   INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
   340        map elem (rev(list next p)) @ xs = Xs}
   341   DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
   342      q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   343   OD
   344   {islist next p \<and> map elem (rev(list next p)) = Xs}"
   345 apply vcg_simp
   346  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
   347 apply fastsimp
   348 done
   349 
   350 
   351 end