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