Theory VcgExTotal

(*
    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
express 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). ⇗s⇖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 < ⇗σ⇖N then ´R = ⇗σ⇖N - 10 else ´R = 91⦄,{}"
  apply (hoare_rule HoareTotal.ProcRec1 [where r="measure (λ(s,p). 101 - ⇗s⇖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 = ⇗σ⇖next x)⦄"
   apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (λ(s,p). length (list ⇗s⇖p ⇗s⇖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 = ⇗σ⇖next x)⦄"
   apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (λ(s,p). length (list ⇗s⇖p ⇗s⇖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 ⇗σ⇖p ⇗σ⇖next Ps ∧  List ⇗σ⇖q ⇗σ⇖next Qs ∧ set Ps ∩ set Qs = {}
     ⟶
     List ´p ´next (Ps@Qs) ∧ (∀x. x∉set Ps ⟶ ´next x = ⇗σ⇖next x)⦄"
   apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (λ(s,p). length (list ⇗s⇖p ⇗s⇖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). (⇗s⇖N + ⇗s⇖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). (⇗s⇖N + ⇗s⇖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). ⇗s⇖N + ⇗s⇖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). ⇗s⇖N) <*mlex*> (λ(s,p). ⇗s⇖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. ⇗s⇖N + ⇗s⇖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