Quelle  Pointer_Examples.thy

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

section ‹Examples of verifications of pointer programs›

theory Pointer_Examples
  imports HeapSyntax
begin

axiomatization where unproven: "PROP A"


subsection "Verifications"

subsubsection "List reversal"

text "A short but unreadable proof:"

lemma "VARS tl p q r
  {List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}}
  WHILE p ≠ Null
  INV {∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
                 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])
  ― ‹explicit:›
  🍋‹apply clarify›
  🍋‹apply(rename_tac ps b qs)›
  🍋‹apply clarsimp›
  🍋‹apply(rename_tac ps')›
  🍋‹apply(fastforce intro:notin_List_update[THEN iffD2])›
  done

text‹And now with ghost variables term‹ps› and term‹qs›. Even
 `more automatic''.›

lemma "VARS next p ps q qs r
  {List next p Ps ∧ List next q Qs ∧ set Ps ∩ set Qs = {} ∧
   ps = Ps ∧ qs = Qs}
  WHILE p ≠ Null
  INV {List next p ps ∧ List next q qs ∧ set ps ∩ set qs = {} ∧
       rev ps @ qs = rev Ps @ Qs}
  DO r := p; p := p^.next; r^.next := q; q := r;
     qs := (hd ps) # qs; ps := tl ps OD
  {List next q (rev Ps @ Qs)}"
apply vcg_simp
 apply fastforce
done

text "A longer readable version:"

lemma "VARS tl p q r
  {List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}}
  WHILE p ≠ Null
  INV {∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
               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) ∧ p ≠ Null"
         (is "(∃ps qs. ?I ps qs) ∧ _")
  then obtain ps qs a where I: "?I ps qs ∧ p = Ref a"
    by fast
  then obtain ps' where "ps = a # ps'" by fastforce
  hence "List (tl(p → q)) (p^.tl) ps' ∧
         List (tl(p → q)) p (a#qs) ∧
         set ps' ∩ set (a#qs) = {} ∧
         rev ps' @ (a#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) ∧ ¬ p ≠ Null"
  thus "List tl q (rev Ps @ Qs)" by fastforce
qed


text‹Finaly, the functional version. A bit more verbose, but automatic!›

lemma "VARS tl p q r
  {islist tl p ∧ islist tl q ∧
   Ps = list tl p ∧ Qs = list tl q ∧ set Ps ∩ set Qs = {}}
  WHILE p ≠ Null
  INV {islist tl p ∧ islist tl q ∧
       set(list tl p) ∩ set(list tl q) = {} ∧
       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 ∧ list tl q = rev Ps @ Qs}"
apply vcg_simp
  apply clarsimp
 apply clarsimp
done


subsubsection "Searching in a list"

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

  start with a proof based on the term‹List› predicate. This means it only
  for acyclic lists.›

lemma "VARS tl p
  {List tl p Ps ∧ X ∈ set Ps}
  WHILE p ≠ Null ∧ p ≠ Ref X
  INV {∃ps. List tl p ps ∧ X ∈ set ps}
  DO p := p^.tl OD
  {p = Ref X}"
apply vcg_simp
  apply blast
 apply clarsimp
apply clarsimp
done

text‹Using term‹Path› instead of term‹List› generalizes the correctness
  to cyclic lists as well:›

lemma "VARS tl p
  {Path tl p Ps X}
  WHILE p ≠ Null ∧ p ≠ X
  INV {∃ps. Path tl p ps X}
  DO p := p^.tl OD
  {p = X}"
apply vcg_simp
  apply blast
 apply fastforce
apply clarsimp
done

text‹Now it dawns on us that we do not need the list witness at all --- it
  to talk about reachability, i.e.\ we can use relations directly. The
  version uses a relation on 🍋‹'a ref›:›

lemma "VARS tl p
  {(p,X) ∈ {(Ref x,tl x) |x. True}^*}
  WHILE p ≠ Null ∧ p ≠ X
  INV {(p,X) ∈ {(Ref x,tl x) |x. True}^*}
  DO p := p^.tl OD
  {p = X}"
apply vcg_simp
 apply clarsimp
 apply(erule converse_rtranclE)
  apply simp
 apply(clarsimp elim:converse_rtranclE)
apply(fast elim:converse_rtranclE)
done

text‹Finally, a version based on a relation on type 🍋‹'a›:›

lemma "VARS tl p
  {p ≠ Null ∧ (addr p,X) ∈ {(x,y). tl x = Ref y}^*}
  WHILE p ≠ Null ∧ p ≠ Ref X
  INV {p ≠ Null ∧ (addr p,X) ∈ {(x,y). tl x = Ref y}^*}
  DO p := p^.tl OD
  {p = Ref X}"
apply vcg_simp
 apply clarsimp
 apply(erule converse_rtranclE)
  apply simp
 apply clarsimp
apply clarsimp
done


subsubsection "Splicing two lists"

lemma "VARS tl p q pp qq
  {List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {} ∧ size Qs ≤ size Ps}
  pp := p;
  WHILE q ≠ Null
  INV {∃as bs qs.
    distinct as ∧ Path tl p as pp ∧ List tl pp bs ∧ List tl q qs ∧
    set bs ∩ set qs = {} ∧ set as ∩ (set bs ∪ set qs) = {} ∧
    size qs ≤ size bs ∧ splice Ps Qs = as @ splice bs qs}
  DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD
  {List tl p (splice Ps Qs)}"
apply vcg_simp
  apply(rule_tac x = "[]" in exI)
  apply fastforce
 apply clarsimp
 apply(rename_tac y bs qqs)
 apply(case_tac bs) apply simp
 apply clarsimp
 apply(rename_tac x bbs)
 apply(rule_tac x = "as @ [x,y]" in exI)
 apply simp
 apply(rule_tac x = "bbs" in exI)
 apply simp
 apply(rule_tac x = "qqs" in exI)
 apply simp
apply (fastforce simp:List_app)
done


subsubsection "Merging two lists"

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

definition cor :: "bool ==> bool ==> bool"
  where "cor P Q ⟷ (if P then True else Q)"

definition cand :: "bool ==> bool ==> bool"
  where "cand P Q ⟷ (if P then Q else False)"

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) = []"

text‹Simplifies the proof a little:›

lemma [simp]: "({} = insert a A ∩ B) = (a ∉ B & {} = A ∩ B)"
by blast
lemma [simp]: "({} = A ∩ insert b B) = (b ∉ A & {} = A ∩ B)"
by blast
lemma [simp]: "({} = A ∩ (B ∪ C)) = ({} = A ∩ B & {} = A ∩ C)"
by blast

lemma "VARS hd tl p q r s
 {List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {} ∧
  (p ≠ Null ∨ q ≠ Null)}
 IF cor (q = Null) (cand (p ≠ Null) (p^.hd ≤ q^.hd))
 THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
 s := r;
 WHILE p ≠ Null ∨ q ≠ Null
 INV {∃rs ps qs a. Path tl r rs s ∧ List tl p ps ∧ List tl q qs ∧
      distinct(a # ps @ qs @ rs) ∧ s = Ref a ∧
      merge(Ps,Qs,λx y. hd x ≤ hd y) =
      rs @ a # merge(ps,qs,λx y. hd x ≤ hd y) ∧
      (tl a = p ∨ tl a = q)}
 DO IF cor (q = Null) (cand (p ≠ Null) (p^.hd ≤ 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,λx y. hd x ≤ hd y))}"
apply vcg_simp
apply (simp_all add: cand_def cor_def)

apply (fastforce)

apply clarsimp
apply(rule conjI)
apply clarsimp
apply(rule conjI)
apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
apply clarsimp
apply(rule conjI)
apply (clarsimp)
apply(rule_tac x = "rs @ [a]" in exI)
apply(clarsimp simp:eq_sym_conv)
apply(rule_tac x = "bs" in exI)
apply(clarsimp simp:eq_sym_conv)
apply(rule_tac x = "ya#bsa" in exI)
apply(simp)
apply(clarsimp simp:eq_sym_conv)
apply(rule_tac x = "rs @ [a]" in exI)
apply(clarsimp simp:eq_sym_conv)
apply(rule_tac x = "y#bs" in exI)
apply(clarsimp simp:eq_sym_conv)
apply(rule_tac x = "bsa" in exI)
apply(simp)
apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)

apply(clarsimp simp add:List_app)
done

text‹And now with ghost variables:›

lemma "VARS elem next p q r s ps qs rs a
 {List next p Ps ∧ List next q Qs ∧ set Ps ∩ set Qs = {} ∧
  (p ≠ Null ∨ q ≠ Null) ∧ ps = Ps ∧ qs = Qs}
 IF cor (q = Null) (cand (p ≠ Null) (p^.elem ≤ q^.elem))
 THEN r := p; p := p^.next; ps := tl ps
 ELSE r := q; q := q^.next; qs := tl qs FI;
 s := r; rs := []; a := addr s;
 WHILE p ≠ Null ∨ q ≠ Null
 INV {Path next r rs s ∧ List next p ps ∧ List next q qs ∧
      distinct(a # ps @ qs @ rs) ∧ s = Ref a ∧
      merge(Ps,Qs,λx y. elem x ≤ elem y) =
      rs @ a # merge(ps,qs,λx y. elem x ≤ elem y) ∧
      (next a = p ∨ next a = q)}
 DO IF cor (q = Null) (cand (p ≠ Null) (p^.elem ≤ q^.elem))
    THEN s^.next := p; p := p^.next; ps := tl ps
    ELSE s^.next := q; q := q^.next; qs := tl qs FI;
    rs := rs @ [a]; s := s^.next; a := addr s
 OD
 {List next r (merge(Ps,Qs,λx y. elem x ≤ elem y))}"
apply vcg_simp
apply (simp_all add: cand_def cor_def)

apply (fastforce)

apply clarsimp
apply(rule conjI)
apply(clarsimp)
apply(rule conjI)
apply(clarsimp simp:neq_commute)
apply(clarsimp simp:neq_commute)
apply(clarsimp simp:neq_commute)

apply(clarsimp simp add:List_app)
done

text‹The proof is a LOT simpler because it does not need
  anymore, but it is still not quite automatic, probably
  of this wrong orientation business.›

text‹More of the previous proof without ghost variables can be
 , but the runtime goes up drastically. In general it is
  more efficient to give the witness directly than to have it
  by proof.

  we try a functional version of the abstraction relation term‹Path›. Since the result is not that convincing, we do not prove any of
  lemmas.›

axiomatization
  ispath :: "('a ==> 'a ref) ==> 'a ref ==> 'a ref ==> bool" and
  path :: "('a ==> 'a ref) ==> 'a ref ==> 'a ref ==> 'a list"

text"First some basic lemmas:"

lemma [simp]: "ispath f p p"
by (rule unproven)
lemma [simp]: "path f p p = []"
by (rule unproven)
lemma [simp]: "ispath f p q ==> a ∉ set(path f p q) ==> ispath (f(a := r)) p q"
by (rule unproven)
lemma [simp]: "ispath f p q ==> a ∉ set(path f p q) ==>
 path (f(a := r)) p q = path f p q"
by (rule unproven)

text"Some more specific lemmas needed by the example:"

lemma [simp]: "ispath (f(a := q)) p (Ref a) ==> ispath (f(a := q)) p q"
by (rule unproven)
lemma [simp]: "ispath (f(a := q)) p (Ref a) ==>
 path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
by (rule unproven)
lemma [simp]: "ispath f p (Ref a) ==> f a = Ref b ==>
 b ∉ set (path f p (Ref a))"
by (rule unproven)
lemma [simp]: "ispath f p (Ref a) ==> f a = Null ==> islist f p"
by (rule unproven)
lemma [simp]: "ispath f p (Ref a) ==> f a = Null ==> list f p = path f p (Ref a) @ [a]"
by (rule unproven)

lemma [simp]: "islist f p ==> distinct (list f p)"
by (rule unproven)

lemma "VARS hd tl p q r s
 {islist tl p ∧ Ps = list tl p ∧ islist tl q ∧ Qs = list tl q ∧
  set Ps ∩ set Qs = {} ∧
  (p ≠ Null ∨ q ≠ Null)}
 IF cor (q = Null) (cand (p ≠ Null) (p^.hd ≤ q^.hd))
 THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
 s := r;
 WHILE p ≠ Null ∨ q ≠ Null
 INV {∃rs ps qs a. ispath tl r s ∧ rs = path tl r s ∧
      islist tl p ∧ ps = list tl p ∧ islist tl q ∧ qs = list tl q ∧
      distinct(a # ps @ qs @ rs) ∧ s = Ref a ∧
      merge(Ps,Qs,λx y. hd x ≤ hd y) =
      rs @ a # merge(ps,qs,λx y. hd x ≤ hd y) ∧
      (tl a = p ∨ tl a = q)}
 DO IF cor (q = Null) (cand (p ≠ Null) (p^.hd ≤ q^.hd))
    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
    s := s^.tl
 OD
 {islist tl r & list tl r = (merge(Ps,Qs,λx y. hd x ≤ hd y))}"
apply vcg_simp

apply (simp_all add: cand_def cor_def)
  apply (fastforce)
 apply (fastforce simp: eq_sym_conv)
apply(clarsimp)
done

text"The proof is automatic, but requires a numbet of special lemmas."


subsubsection "Cyclic list reversal"


text‹We consider two algorithms for the reversal of circular lists.
 ›

lemma circular_list_rev_I:
  "VARS next root p q tmp
  {root = Ref r ∧ distPath next root (r#Ps) root}
  p := root; q := root^.next;
  WHILE q ≠ root
  INV {∃ ps qs. distPath next p ps root ∧ distPath next q qs root ∧
             root = Ref r ∧ r ∉ set Ps ∧ set ps ∩ set qs = {} ∧
             Ps = (rev ps) @ qs }
  DO tmp := q; q := q^.next; tmp^.next := p; p:=tmp OD;
  root^.next := p
  { root = Ref r ∧ distPath next root (r#rev Ps) root}"
apply (simp only:distPath_def)
apply vcg_simp
  apply (rule_tac x="[]" in exI)
  apply auto
 apply (drule (2) neq_dP)
 apply clarsimp
 apply(rule_tac x="a # ps" in exI)
apply clarsimp
done

text‹In the beginning, we are able to assert term‹distPath next
  as root›, with term‹as› set to term‹[]› or
 term‹[r,a,b,c]›. Note that term‹Path next root as root› would
  give us an infinite number of lists with the recurring
  term‹[r,a,b,c]›.

  precondition states that there exists a non-empty non-repeating
  \mbox{term‹r # Ps›} from pointer term‹root› to itself, given that
 term‹root› points to location term‹r›. Pointers term‹p› and
 term‹q› are then set to term‹root› and the successor of term‹root› respectively. If term‹q = root›, we have circled the loop,
  we set the term‹next› pointer field of term‹q› to point
  term‹p›, and shift term‹p› and term‹q› one step forward. The
  thus states that term‹p› and term‹q› point to two
  lists term‹ps› and term‹qs›, such that term‹Ps = rev ps
  qs›. After the loop terminates, one
  step is needed to close the loop. As expected, the postcondition
  that the term‹distPath› from term‹root› to itself is now
 term‹r # (rev Ps)›.

  may come as a surprise to the reader that the simple algorithm for
  list reversal, with modified annotations, works for cyclic
  as well:›


lemma circular_list_rev_II:
"VARS next p q tmp
{p = Ref r ∧ distPath next p (r#Ps) p}
q:=Null;
WHILE p ≠ Null
INV
{ ((q = Null) ⟶ (∃ps. distPath next p (ps) (Ref r) ∧ ps = r#Ps)) ∧
  ((q ≠ Null) ⟶ (∃ps qs. distPath next q (qs) (Ref r) ∧ List next p ps ∧
                   set ps ∩ set qs = {} ∧ rev qs @ ps = Ps@[r])) ∧
  ¬ (p = Null ∧ q = Null) }
DO tmp := p; p := p^.next; tmp^.next := q; q:=tmp OD
{q = Ref r ∧ distPath next q (r # rev Ps) q}"
apply (simp only:distPath_def)
apply vcg_simp
  apply clarsimp
 apply (case_tac "(q = Null)")
  apply (fastforce intro: Path_is_List)
 apply clarsimp
 apply (rule_tac x= "bs" in exI)
 apply (rule_tac x= "y # qs" in exI)
 apply clarsimp
apply (auto simp:fun_upd_apply)
done


subsubsection "Storage allocation"

definition new :: "'a set ==> 'a"
  where "new A = (SOME a. a ∉ A)"


lemma new_notin:
 "[ ~finite(UNIV::'a set); finite(A::'a set); B ⊆ A ] ==> new (A) ∉ B"
apply(unfold new_def)
apply(rule someI2_ex)
 apply (fast intro:ex_new_if_finite)
apply (fast)
done


lemma "~finite(UNIV::'a set) ==>
  VARS xs elem next alloc p q
  {Xs = xs ∧ p = (Null::'a ref)}
  WHILE xs ≠ []
  INV {islist next p ∧ set(list next p) ⊆ set alloc ∧
       map elem (rev(list next p)) @ xs = Xs}
  DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
     q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
  OD
  {islist next p ∧ 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