Quelle Pointers0.thy Sprache: Isabelle

(*  Title:      HOL/Hoare/Pointers0.thy
    Author:     Tobias Nipkow
    Copyright   2002 TUM

This is like Pointers.thy, but instead of a type constructor 'a ref
that adjoins Null to a type, Null is simply a distinguished element of
the address type. This avoids the Ref constructor and thus simplifies
specifications (a bit). However, the proofs don't seem to get simpler
- in fact in some case they appear to get (a bit) more complicated.
*)

section \<open>Alternative pointers\<close>

theory Pointers0
  imports Hoare_Logic
begin

subsection "References"

class ref =
  fixes Null :: 'a

subsection "Field access and update"

syntax
  "_fassign"  :: "'a::ref => id => 'v => 's com"
    (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare field assignment\<close>\<close>_^._ :=/ _)\<close> [70,1000,65] 61)
  "_faccess"  :: "'a::ref => ('a::ref \ 'v) => 'v"
    (\<open>(\<open>open_block notation=\<open>mixfix Hoare field access\<close>\<close>_^._)\<close> [65,1000] 65)
translations
  "p^.f := e"  =>  "f := CONST fun_upd f p e"
  "p^.f"       =>  "f p"

text "An example due to Suzuki:"

lemma "VARS v n
  {distinct[w,x,y,z]}
  w^.v := (1::int); w^.n := x;
  x^.v := 2; x^.n := y;
  y^.v := 3; y^.n := z;
  z^.v := 4; x^.n := z
  {w^.n^.n^.v = 4}"
by vcg_simp

subsection "The heap"

subsubsection "Paths in the heap"

primrec Path :: "('a::ref \ 'a) \ 'a \ 'a list \ 'a \ bool"
where
  "Path h x [] y = (x = y)"
| "Path h x (a#as) y = (x \ Null \ x = a \ Path h (h a) as y)"

lemma [iff]: "Path h Null xs y = (xs = [] \ y = Null)"
apply(case_tac xs)
apply fastforce
apply fastforce
done

lemma [simp]: "a \ Null \ Path h a as z =
(as = [] \<and> z = a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
apply(case_tac as)
apply fastforce
apply fastforce
done

lemma [simp]: "\x. Path f x (as@bs) z = (\y. Path f x as y \ Path f y bs z)"
by(induct as, simp+)

lemma [simp]: "\x. u \ set as \ Path (f(u := v)) x as y = Path f x as y"
by(induct as, simp, simp add:eq_sym_conv)

subsubsection "Lists on the heap"

paragraph "Relational abstraction"

definition List :: "('a::ref \ 'a) \ 'a \ 'a list \ bool"
  where "List h x as = Path h x as Null"

lemma [simp]: "List h x [] = (x = Null)"
by(simp add:List_def)

lemma [simp]: "List h x (a#as) = (x \ Null \ x = a \ List h (h a) as)"
by(simp add:List_def)

lemma [simp]: "List h Null as = (as = [])"
by(case_tac as, simp_all)

lemma List_Ref[simp]:
"a \ Null \ List h a as = (\bs. as = a#bs \ List h (h a) bs)"
by(case_tac as, simp_all, fast)

theorem notin_List_update[simp]:
"\x. a \ set as \ List (h(a := y)) x as = List h x as"
apply(induct as)
apply simp
apply(clarsimp simp add:fun_upd_apply)
done

declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp]

lemma List_unique: "\x bs. List h x as \ List h x bs \ as = bs"
by(induct as, simp, clarsimp)

lemma List_unique1: "List h p as \ \!as. List h p as"
by(blast intro:List_unique)

lemma List_app: "\x. List h x (as@bs) = (\y. Path h x as y \ List h y bs)"
by(induct as, simp, clarsimp)

lemma List_hd_not_in_tl[simp]: "List h (h a) as \ a \ set as"
apply (clarsimp simp add:in_set_conv_decomp)
apply(frule List_app[THEN iffD1])
apply(fastforce dest: List_unique)
done

lemma List_distinct[simp]: "\x. List h x as \ distinct as"
apply(induct as, simp)
apply(fastforce dest:List_hd_not_in_tl)
done

subsubsection "Functional abstraction"

definition islist :: "('a::ref \ 'a) \ 'a \ bool"
  where "islist h p \ (\as. List h p as)"

definition list :: "('a::ref \ 'a) \ 'a \ 'a list"
  where "list h p = (SOME as. List h p as)"

lemma List_conv_islist_list: "List h p as = (islist h p \ as = list h p)"
apply(simp add:islist_def list_def)
apply(rule iffI)
apply(rule conjI)
apply blast
apply(subst some1_equality)
  apply(erule List_unique1)
apply assumption
apply(rule refl)
apply simp
apply(rule someI_ex)
apply fast
done

lemma [simp]: "islist h Null"
by(simp add:islist_def)

lemma [simp]: "a \ Null \ islist h a = islist h (h a)"
by(simp add:islist_def)

lemma [simp]: "list h Null = []"
by(simp add:list_def)

lemma list_Ref_conv[simp]:
"\ a \ Null; islist h (h a) \ \ list h a = a # list h (h a)"
apply(insert List_Ref[of _ h])
apply(fastforce simp:List_conv_islist_list)
done

lemma [simp]: "islist h (h a) \ a \ set(list h (h a))"
apply(insert List_hd_not_in_tl[of h])
apply(simp add:List_conv_islist_list)
done

lemma list_upd_conv[simp]:
"islist h p \ y \ set(list h p) \ list (h(y := q)) p = list h p"
apply(drule notin_List_update[of _ _ h q p])
apply(simp add:List_conv_islist_list)
done

lemma islist_upd[simp]:
"islist h p \ y \ set(list h p) \ islist (h(y := q)) p"
apply(frule notin_List_update[of _ _ h q p])
apply(simp add:List_conv_islist_list)
done

subsection "Verifications"

subsubsection "List reversal"

text "A short but unreadable proof:"

lemma "VARS tl p q r
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
  WHILE p \<noteq> Null
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                 rev ps @ qs = rev Ps @ Qs}
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
  {List tl q (rev Ps @ Qs)}"
apply vcg_simp
  apply fastforce
  apply(fastforce intro:notin_List_update[THEN iffD2])
  \<comment> \<open>explicit:\<close>
  \<^cancel>\<open>apply clarify\<close>
  \<^cancel>\<open>apply(rename_tac ps qs)\<close>
  \<^cancel>\<open>apply clarsimp\<close>
  \<^cancel>\<open>apply(rename_tac ps')\<close>
  \<^cancel>\<open>apply(rule_tac x = ps' in exI)\<close>
  \<^cancel>\<open>apply simp\<close>
  \<^cancel>\<open>apply(rule_tac x = "p#qs" in exI)\<close>
  \<^cancel>\<open>apply simp\<close>
  done

text "A longer readable version:"

lemma "VARS tl p q r
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
  WHILE p \<noteq> Null
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @ qs = rev Ps @ Qs}
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
  {List tl q (rev Ps @ Qs)}"
proof vcg
  fix tl p q r
  assume "List tl p Ps \ List tl q Qs \ set Ps \ set Qs = {}"
  thus "\ps qs. List tl p ps \ List tl q qs \ set ps \ set qs = {} \
                rev ps @ qs = rev Ps @ Qs" by fastforce
next
  fix tl p q r
  assume "(\ps qs. List tl p ps \ List tl q qs \ set ps \ set qs = {} \
                   rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
         (is "(\ps qs. ?I ps qs) \ _")
  then obtain ps qs where I: "?I ps qs \ p \ Null" by fast
  then obtain ps' where "ps = p # ps'" by fastforce
  hence "List (tl(p := q)) (p^.tl) ps' \
         List (tl(p := q)) p       (p#qs) \<and>
         set ps' \ set (p#qs) = {} \
         rev ps' @ (p#qs) = rev Ps @ Qs"
    using I by fastforce
  thus "\ps' qs'. List (tl(p := q)) (p^.tl) ps' \
                  List (tl(p := q)) p       qs' \
                  set ps' \ set qs' = {} \
                  rev ps' @ qs' = rev Ps @ Qs" by fast
next
  fix tl p q r
  assume "(\ps qs. List tl p ps \ List tl q qs \ set ps \ set qs = {} \
                   rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
  thus "List tl q (rev Ps @ Qs)" by fastforce
qed

text\<open>Finaly, the functional version. A bit more verbose, but automatic!\<close>

lemma "VARS tl p q r
  {islist tl p \<and> islist tl q \<and>
   Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
  WHILE p \<noteq> Null
  INV {islist tl p \<and> islist tl q \<and>
       set(list tl p) \<inter> set(list tl q) = {} \<and>
       rev(list tl p) @ (list tl q) = rev Ps @ Qs}
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
  {islist tl q \<and> list tl q = rev Ps @ Qs}"
apply vcg_simp
  apply clarsimp
apply clarsimp
done

subsubsection "Searching in a list"

text\<open>What follows is a sequence of successively more intelligent proofs that
a simple loop finds an element in a linked list.

We start with a proof based on the \<^term>\<open>List\<close> predicate. This means it only
works for acyclic lists.\<close>

lemma "VARS tl p
  {List tl p Ps \<and> X \<in> set Ps}
  WHILE p \<noteq> Null \<and> p \<noteq> X
  INV {p \<noteq> Null \<and> (\<exists>ps. List tl p ps \<and> X \<in> set ps)}
  DO p := p^.tl OD
  {p = X}"
apply vcg_simp
  apply(case_tac "p = Null")
   apply clarsimp
  apply fastforce
apply clarsimp
apply fastforce
apply clarsimp
done

text\<open>Using \<^term>\<open>Path\<close> instead of \<^term>\<open>List\<close> generalizes the correctness
statement to cyclic lists as well:\<close>

lemma "VARS tl p
  {Path tl p Ps X}
  WHILE p \<noteq> Null \<and> p \<noteq> X
  INV {\<exists>ps. Path tl p ps X}
  DO p := p^.tl OD
  {p = X}"
apply vcg_simp
  apply blast
apply fastforce
apply clarsimp
done

text\<open>Now it dawns on us that we do not need the list witness at all --- it
suffices to talk about reachability, i.e.\ we can use relations directly.\<close>

lemma "VARS tl p
  {(p,X) \<in> {(x,y). y = tl x & x \<noteq> Null}\<^sup>*}
  WHILE p \<noteq> Null \<and> p \<noteq> X
  INV {(p,X) \<in> {(x,y). y = tl x & x \<noteq> Null}\<^sup>*}
  DO p := p^.tl OD
  {p = X}"
apply vcg_simp
apply clarsimp
apply(erule converse_rtranclE)
  apply simp
apply(simp)
apply(fastforce elim:converse_rtranclE)
done

subsubsection "Merging two lists"

text"This is still a bit rough, especially the proof."

fun merge :: "'a list * 'a list * ('a \ 'a \ bool) \ 'a list" where
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
                                else y # merge(x#xs,ys,f))" |
"merge(x#xs,[],f) = x # merge(xs,[],f)" |
"merge([],y#ys,f) = y # merge([],ys,f)" |
"merge([],[],f) = []"

lemma imp_disjCL: "(P|Q \ R) = ((P \ R) \ (~P \ Q \ R))"
by blast

declare disj_not1[simp del] imp_disjL[simp del] imp_disjCL[simp]

lemma "VARS hd tl p q r s
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
  (p \<noteq> Null \<or> q \<noteq> Null)}
IF if q = Null then True else p ~= Null & p^.hd \<le> q^.hd
THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
s := r;
WHILE p \<noteq> Null \<or> q \<noteq> Null
INV {\<exists>rs ps qs. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
      distinct(s # ps @ qs @ rs) \<and> s \<noteq> Null \<and>
      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
      rs @ s # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
      (tl s = p \<or> tl s = q)}
DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
    s := s^.tl
OD
{List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
apply vcg_simp

apply (fastforce)

apply clarsimp
apply(rule conjI)
apply clarsimp
apply(simp add:eq_sym_conv)
apply(rule_tac x = "rs @ [s]" in exI)
apply simp
apply(rule_tac x = "bs" in exI)
apply (fastforce simp:eq_sym_conv)

apply clarsimp
apply(rule conjI)
apply clarsimp
apply(rule_tac x = "rs @ [s]" in exI)
apply simp
apply(rule_tac x = "bsa" in exI)
apply(rule conjI)
apply (simp add:eq_sym_conv)
apply(rule exI)
apply(rule conjI)
apply(rule_tac x = bs in exI)
apply(rule conjI)
apply(rule refl)
apply (simp add:eq_sym_conv)
apply (simp add:eq_sym_conv)

apply(rule conjI)
apply clarsimp
apply(rule_tac x = "rs @ [s]" in exI)
apply simp
apply(rule_tac x = bs in exI)
apply (simp add:eq_sym_conv)
apply clarsimp
apply(rule_tac x = "rs @ [s]" in exI)
apply (simp add:eq_sym_conv)
apply(rule exI)
apply(rule conjI)
apply(rule_tac x = bsa in exI)
apply(rule conjI)
apply(rule refl)
apply (simp add:eq_sym_conv)
apply(rule_tac x = bs in exI)
apply (simp add:eq_sym_conv)

apply(clarsimp simp add:List_app)
done

(* TODO: merging with islist/list instead of List: an improvement?
   needs (is)path, which is not so easy to prove either. *)

subsubsection "Storage allocation"

definition new :: "'a set \ 'a::ref"
  where "new A = (SOME a. a \ A & a \ Null)"

lemma new_notin:
"\ ~finite(UNIV::('a::ref)set); finite(A::'a set); B \ A \ \
  new (A) \<notin> B & new A \<noteq> Null"
apply(unfold new_def)
apply(rule someI2_ex)
apply (fast dest:ex_new_if_finite[of "insert Null A"])
apply (fast)
done

lemma "~finite(UNIV::('a::ref)set) \
  VARS xs elem next alloc p q
  {Xs = xs \<and> p = (Null::'a)}
  WHILE xs \<noteq> []
  INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
       map elem (rev(list next p)) @ xs = Xs}
  DO q := new(set alloc); alloc := q#alloc;
     q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
  OD
  {islist next p \<and> map elem (rev(list next p)) = Xs}"
apply vcg_simp
apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
done

end

quality99%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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 ist noch experimentell.