Quelle  VcgExTotal.thy

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer

*)

section ‹Examples for Total Correctness›

theory VcgExTotal imports "../HeapList" "../Vcg" begin

record 'g vars = "'g state" +
  A_' :: nat
  I_' :: nat
  M_' :: nat
  N_' :: nat
  R_' :: nat
  S_' :: nat
  Abr_':: string


lemma "Γ⊨_t {🍋M = 0 ∧ 🍋S = 0}
          WHILE 🍋M ≠ a
          INV {🍋S = 🍋M * b ∧ 🍋M ≤ a}
          VAR MEASURE a - 🍋M
          DO 🍋S :== 🍋S + b;; 🍋M :== 🍋M + 1 OD
          {🍋S = a * b}"
apply vcg
apply (auto)
done

lemma "Γ⊨_t {🍋I ≤ 3}
     WHILE 🍋I < 10 INV {🍋I≤ 10} VAR MEASURE 10 - 🍋I
     DO
       🍋I :== 🍋I + 1
     OD
  {🍋I = 10}"
apply vcg
apply auto
done

text ‹Total correctness of a nested loop. In the inner loop we have to
  that the loop variable of the outer loop is not changed. We use
 ‹FIX› to introduce a new logical variable
 ›

lemma "Γ⊨_t {🍋M=0 ∧ 🍋N=0}
      WHILE (🍋M < i)
      INV {🍋M ≤ i ∧ (🍋M ≠ 0 ⟶ 🍋N = j) ∧ 🍋N ≤ j}
      VAR MEASURE (i - 🍋M)
      DO
         🍋N :== 0;;
         WHILE (🍋N < j)
         FIX m.
         INV {🍋M=m ∧ 🍋N ≤ j}
         VAR MEASURE (j - 🍋N)
         DO
           🍋N :== 🍋N + 1
         OD;;
       🍋M :== 🍋M + 1
       OD
       {🍋M=i ∧ (🍋M≠0 ⟶ 🍋N=j)}"
apply vcg
apply simp_all
apply arith
done

primrec fac:: "nat ==> nat"
where
"fac 0 = 1" |
"fac (Suc n) = (Suc n) * fac n"

lemma fac_simp [simp]: "0 < i ==> fac i = i * fac (i - 1)"
  by (cases i) simp_all

procedures
  Fac (N | R) = "IF 🍋N = 0 THEN 🍋R :== 1
                       ELSE CALL Fac(🍋N - 1,🍋R);;
                            🍋R :== 🍋N * 🍋R
                       FI"

lemma (in Fac_impl) Fac_spec:
  shows "∀n. Γ⊨_t {🍋N=n} 🍋R :== PROC Fac(🍋N) {🍋R = fac n}"
  apply (hoare_rule HoareTotal.ProcRec1 [where r="measure (λ(s,p). N)"])
  apply vcg
  apply simp
  done



procedures
  p91(R,N | R) = "IF 100 < 🍋N THEN 🍋R :== 🍋N - 10
                      ELSE 🍋R :== CALL p91(🍋R,🍋N+11);;
                           🍋R :== CALL p91(🍋R,🍋R) FI"


  p91_spec: "∀n. Γ⊨_t {🍋N=n} 🍋R :== PROC p91(🍋R,🍋N)
                        {if 100 < n then 🍋R = n - 10 else 🍋R = 91},{}"

lemma (in p91_impl) p91_spec:
  shows "∀σ. Γ⊨_t {σ} 🍋R :== PROC p91(🍋R,🍋N)
                       {if 100 < ^<sigma>N then 🍋R = ^<sigma>N - 10 else 🍋R = 91},{}"
  apply (hoare_rule HoareTotal.ProcRec1 [where r="measure (λ(s,p). 101 - N)"])
  apply vcg
  apply clarsimp
  apply arith
  done

record globals_list =
  next_' :: "ref ==> ref"
  cont_' :: "ref ==> nat"

record 'g list_vars = "'g state" +
  p_'    :: "ref"
  q_'    :: "ref"
  r_'    :: "ref"
  root_' :: "ref"
  tmp_'  :: "ref"

procedures
  append(p,q|p) =
    "IF 🍋p=Null THEN 🍋p :== 🍋q ELSE 🍋p→🍋next :== CALL append(🍋p→🍋next,🍋q) FI"

lemma (in append_impl)
  shows
   "∀σ Ps Qs. Γ⊨_t
      {σ. List 🍋p 🍋next Ps ∧ List 🍋q 🍋next Qs ∧ set Ps ∩ set Qs = {} }
       🍋p :== PROC append(🍋p,🍋q)
      {List 🍋p 🍋next (Ps@Qs) ∧ (∀x. x∉set Ps ⟶ 🍋next x = ^<sigma>next x)}"
   apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (λ(s,p). length (list p next))"])
   apply vcg
   apply (fastforce  simp add: List_list)
   done


lemma (in append_impl)
  shows
   "∀σ Ps Qs. Γ⊨_t
      {σ. List 🍋p 🍋next Ps ∧ List 🍋q 🍋next Qs ∧ set Ps ∩ set Qs = {} }
       🍋p :== PROC append(🍋p,🍋q)
      {List 🍋p 🍋next (Ps@Qs) ∧ (∀x. x∉set Ps ⟶ 🍋next x = ^<sigma>next x)}"
   apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (λ(s,p). length (list p next))"])
   apply vcg
   apply (fastforce  simp add: List_list)
   done

lemma (in append_impl)
  shows
  append_spec:
   "∀σ. Γ⊨_t ({σ} ∩ {islist 🍋p 🍋next}) 🍋p :== PROC append(🍋p,🍋q)
    {∀Ps Qs. List ^<sigma>p ^<sigma>next Ps ∧ List ^<sigma>q ^<sigma>next Qs ∧ set Ps ∩ set Qs = {}
     ⟶
     List 🍋p 🍋next (Ps@Qs) ∧ (∀x. x∉set Ps ⟶ 🍋next x = ^<sigma>next x)}"
   apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (λ(s,p). length (list p next))"])
   apply vcg
   apply fastforce
   done

lemma "Γ⊨{List 🍋p 🍋next Ps}
       🍋q :== Null;;
       WHILE 🍋p ≠ Null INV {∃Ps' Qs'. List 🍋p 🍋next Ps' ∧ List 🍋q 🍋next Qs' ∧
                             set Ps' ∩ set Qs' = {} ∧
                             rev Ps' @ Qs' = rev Ps}
        DO
         🍋r :== 🍋p;; 🍋p :== 🍋p→🍋next;;
         🍋r→🍋next :== 🍋q;; 🍋q :== 🍋r
       OD;;
       🍋p :==🍋q
       {List 🍋p 🍋next (rev Ps)} "
apply vcg
apply   clarsimp
apply  clarsimp
apply force
apply simp
done

lemma conjI2: "[Q; Q ==> P] ==> P ∧ Q"
by blast

procedures Rev(p|p) =
      "🍋q :== Null;;
       WHILE 🍋p ≠ Null
       DO
         🍋r :== 🍋p;; {🍋p ≠ Null}⟼ 🍋p :== 🍋p→🍋next;;
         {🍋r ≠ Null}⟼ 🍋r→🍋next :== 🍋q;; 🍋q :== 🍋r
       OD;;
       🍋p :==🍋q"
 Rev_spec:
  "∀Ps. Γ⊨_t {List 🍋p 🍋next Ps} 🍋p :== PROC Rev(🍋p) {List 🍋p 🍋next (rev Ps)}"
 Rev_modifies:
  "∀σ. Γ⊨_UNIV {σ} 🍋p :== PROC Rev(🍋p) {t. t may_only_modify_globals σ in [next]}"

text ‹We only need partial correctness of modifies clause!›



lemma upd_hd_next:
  assumes p_ps: "List p next (p#ps)"
  shows "List (next p) (next(p := q)) ps"
proof -
  from p_ps
  have "p ∉ set ps"
    by auto
  with p_ps show ?thesis
    by simp
qed

lemma (in Rev_impl) shows
 Rev_spec:
  "∀Ps. Γ⊨_t {List 🍋p 🍋next Ps} 🍋p :== PROC Rev(🍋p) {List 🍋p 🍋next (rev Ps)}"
apply (hoare_rule HoareTotal.ProcNoRec1)
apply (hoare_rule anno =
       "🍋q :== Null;;
       WHILE 🍋p ≠ Null INV {∃Ps' Qs'. List 🍋p 🍋next Ps' ∧ List 🍋q 🍋next Qs' ∧
                             set Ps' ∩ set Qs' = {} ∧
                             rev Ps' @ Qs' = rev Ps}
       VAR MEASURE (length (list 🍋p 🍋next) )
        DO
         🍋r :== 🍋p;; {🍋p ≠ Null}⟼🍋p :== 🍋p→🍋next;;
         {🍋r ≠ Null}⟼🍋r→🍋next :== 🍋q;; 🍋q :== 🍋r
       OD;;
       🍋p :==🍋q" in HoareTotal.annotateI)
apply vcg
apply   clarsimp
apply  clarsimp
apply  (rule conjI2)
apply   force
apply  clarsimp
apply  (subgoal_tac "List p next (p#ps)")
prefer 2 apply simp
apply  (frule_tac q=q in upd_hd_next)
apply  (simp only: List_list)
apply  simp
apply simp
done


lemma (in Rev_impl) shows
 Rev_modifies:
  "∀σ. Γ⊨_UNIV {σ} 🍋p :== PROC Rev(🍋p) {t. t may_only_modify_globals σ in [next]}"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (vcg spec=modifies)
done

lemma "Γ⊨_t {List 🍋p 🍋next Ps}
       🍋q :== Null;;
       WHILE 🍋p ≠ Null INV {∃Ps' Qs'. List 🍋p 🍋next Ps' ∧ List 🍋q 🍋next Qs' ∧
                             set Ps' ∩ set Qs' = {} ∧
                             rev Ps' @ Qs' = rev Ps}
       VAR MEASURE (length (list 🍋p 🍋next) )
        DO
         🍋r :== 🍋p;; 🍋p :== 🍋p→🍋next;;
         🍋r→🍋next :== 🍋q;; 🍋q :== 🍋r
       OD;;
       🍋p :==🍋q
       {List 🍋p 🍋next (rev Ps)} "
apply vcg
apply   clarsimp
apply  clarsimp
apply  (rule conjI2)
apply   force
apply  clarsimp
apply  (subgoal_tac "List p next (p#ps)")
prefer 2 apply simp
apply  (frule_tac q=q in upd_hd_next)
apply  (simp only: List_list)
apply  simp
apply simp
done




procedures
  pedal(N,M) = "IF 0 < 🍋N THEN
                            IF 0 < 🍋M THEN CALL coast(🍋N- 1,🍋M- 1) FI;;
                            CALL pedal(🍋N- 1,🍋M)
                         FI"

and

  coast(N,M) = "CALL pedal(🍋N,🍋M);;
                         IF 0 < 🍋M THEN CALL coast(🍋N,🍋M- 1) FI"


ML ‹ML_Thms.bind_thm ("HoareTotal_ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Total 2)›


lemma (in pedal_coast_clique)
  shows "(Γ⊨_t {True} PROC pedal(🍋N,🍋M) {True}) ∧
         (Γ⊨_t {True} PROC coast(🍋N,🍋M) {True})"
  apply (hoare_rule HoareTotal_ProcRec2
          [where ?r= "inv_image (measure (λm. m) <*lex*>
                                  measure (λp. if p = coast_'proc then 1 else 0))
                      (λ(s,p). (N + M,p))"])
  apply simp_all
  apply  vcg
  apply  simp
  apply vcg
  apply simp
  done

lemma (in pedal_coast_clique)
  shows "(Γ⊨_t {True} PROC pedal(🍋N,🍋M) {True}) ∧
         (Γ⊨_t {True} PROC coast(🍋N,🍋M) {True})"
  apply (hoare_rule HoareTotal_ProcRec2
          [where ?r= "inv_image (measure (λm. m) <*lex*>
                                  measure (λp. if p = coast_'proc then 1 else 0))
                      (λ(s,p). (N + M,p))"])
  apply simp_all
  apply  vcg
  apply  simp
  apply vcg
  apply simp
  done




lemma (in pedal_coast_clique)
  shows "(Γ⊨_t {True} PROC pedal(🍋N,🍋M) {True}) ∧
         (Γ⊨_t {True} PROC coast(🍋N,🍋M) {True})"
  apply(hoare_rule HoareTotal_ProcRec2
     [where ?r= "measure (λ(s,p). N + M + (if p = coast_'proc then 1 else 0))"])
  apply simp_all
  apply  vcg
  apply  simp
  apply  arith
  apply vcg
  apply simp
  done


lemma (in pedal_coast_clique)
  shows "(Γ⊨_t {True} PROC pedal(🍋N,🍋M) {True}) ∧
         (Γ⊨_t {True} PROC coast(🍋N,🍋M) {True})"
  apply(hoare_rule HoareTotal_ProcRec2
     [where ?r= "(λ(s,p). N) <*mlex*> (λ(s,p). M) <*mlex*>
                 measure (λ(s,p). if p = coast_'proc then 1 else 0)"])
   apply  simp_all
   apply  vcg
   apply  simp
   apply vcg
   apply simp
   done


lemma (in pedal_coast_clique)
  shows "(Γ⊨_t {True} PROC pedal(🍋N,🍋M) {True}) ∧
         (Γ⊨_t {True} PROC coast(🍋N,🍋M) {True})"
  apply(hoare_rule HoareTotal_ProcRec2
     [where ?r= "measure (λs. N + M) <*lex*>
                 measure (λp. if p = coast_'proc then 1 else 0)"])
   apply simp_all
   apply  vcg
   apply  simp
   apply vcg
   apply simp
   done


end