Quelle  OG_Hoare.thy

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹ Owicki-Gries for Partial Correctness ›
theory OG_Hoare
imports OG_Annotations 
begin

subsection ‹Validity of Hoare Tuples: ‹Γ⊨_F P c Q,A››

definition
  valid :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] => bool"
                (‹_ ⊨_{/_}/ _ _ _, _›  [61,60,1000, 20, 1000,1000] 60)
where
  "Γ ⊨_F P c Q,A ≡ ∀s t c'. Γ⊨(c,s) →^* (c', t) ⟶ final (c', t ) ⟶ s ∈ Normal ` P ⟶ t ∉ Fault ` F
                      ⟶ c' = Skip ∧ t ∈ Normal ` Q ∨ c' = Throw ∧ t ∈ Normal ` A"

subsection ‹Interference Freedom›

inductive
 atomicsR :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> ('s, 'p, 'f) ann ==> ('s,'p,'f) com ==> ('s assn × ('s, 'p, 'f) com) ==> bool"
  for Γ::"('s,'p,'f) body"
  and Θ :: " ('s,'p,'f) proc_assns"
where
  AtBasic: "atomicsR Γ Θ (AnnExpr p) (Basic f) (p, Basic f)"
| AtSpec: "atomicsR Γ Θ (AnnExpr p) (Spec r) (p, Spec r)"
| AtAwait: "atomicsR Γ Θ (AnnRec r ae) (Await b e) (r ∩ b, Await b e)"
| AtWhileExpr: "atomicsR Γ Θ p e a ==> atomicsR Γ Θ (AnnWhile r i p) (While b e) a"
| AtGuardExpr: "atomicsR Γ Θ p e a ==> atomicsR Γ Θ (AnnRec r p) (Guard f b e) a" 
| AtDynCom: "x ∈ r ==> atomicsR Γ Θ ad (f x) a ==> atomicsR Γ Θ (AnnRec r ad) (DynCom f) a" 
| AtCallExpr: "Γ f = Some b ==> Θ f = Some as ==>
                n < length as ==>
                atomicsR Γ Θ (as!n) b a ==>
               atomicsR Γ Θ (AnnCall r n) (Call f) a"
| AtSeqExpr1: "atomicsR Γ Θ a1 c1 a ==>
               atomicsR Γ Θ (AnnComp a1 a2) (Seq c1 c2) a" 
| AtSeqExpr2: "atomicsR Γ Θ a2 c2 a ==>
               atomicsR Γ Θ (AnnComp a1 a2) (Seq c1 c2) a" 
| AtCondExpr1: "atomicsR Γ Θ a1 c1 a ==>
               atomicsR Γ Θ (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AtCondExpr2: "atomicsR Γ Θ a2 c2 a ==>
               atomicsR Γ Θ (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AtCatchExpr1: "atomicsR Γ Θ a1 c1 a ==>
               atomicsR Γ Θ (AnnComp a1 a2) (Catch c1 c2) a" 
| AtCatchExpr2: "atomicsR Γ Θ a2 c2 a ==>
               atomicsR Γ Θ (AnnComp a1 a2) (Catch c1 c2) a" 
| AtParallelExprs: "i < length cs ==> atomicsR Γ Θ (fst (as!i)) (cs!i) a ==>
    atomicsR Γ Θ (AnnPar as) (Parallel cs) a"

lemma atomicsR_Skip[simp]:
  "atomicsR Γ Θ a Skip r = False"
 by (auto elim: atomicsR.cases)

lemma atomicsR_Throw[simp]:
  "atomicsR Γ Θ a Throw r = False"
 by (auto elim: atomicsR.cases)

inductive
 assertionsR :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> 's assn ==> 's assn ==> ('s, 'p, 'f) ann ==> ('s,'p,'f) com ==> 's assn ==> bool"
  for Γ::"('s,'p,'f) body"
  and Θ :: " ('s,'p,'f) proc_assns"
where
  AsSkip: "assertionsR Γ Θ Q A (AnnExpr p) Skip p"
| AsThrow: "assertionsR Γ Θ Q A (AnnExpr p) Throw p"
| AsBasic: "assertionsR Γ Θ Q A (AnnExpr p) (Basic f) p"
| AsBasicSkip: "assertionsR Γ Θ Q A (AnnExpr p) (Basic f) Q"
| AsSpec: "assertionsR Γ Θ Q A (AnnExpr p) (Spec r) p"
| AsSpecSkip: "assertionsR Γ Θ Q A (AnnExpr p) (Spec r) Q"
| AsAwaitSkip: "assertionsR Γ Θ Q A (AnnRec r ae) (Await b e) Q"
| AsAwaitThrow: "assertionsR Γ Θ Q A (AnnRec r ae) (Await b e) A"
| AsAwait: "assertionsR Γ Θ Q A (AnnRec r ae) (Await b e) r"
| AsWhileExpr: "assertionsR Γ Θ i A p e a ==> assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) a" 
| AsWhileAs: "assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) r"
| AsWhileInv: "assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) i"
| AsWhileSkip: "assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) Q"
| AsGuardExpr: "assertionsR Γ Θ Q A p e a ==> assertionsR Γ Θ Q A (AnnRec r p) (Guard f b e) a" 
| AsGuardAs: "assertionsR Γ Θ Q A (AnnRec r p) (Guard f b e) r" 
| AsDynComExpr: "x ∈ r ==> assertionsR Γ Θ Q A ad (f x) a ==> assertionsR Γ Θ Q A (AnnRec r ad) (DynCom f) a" 
| AsDynComAs: "assertionsR Γ Θ Q A (AnnRec r p) (DynCom f) r" 
| AsCallAs: "assertionsR Γ Θ Q A (AnnCall r n) (Call f) r" 
| AsCallExpr: "Γ f = Some b ==> Θ f = Some as ==>
                n < length as ==>
                assertionsR Γ Θ Q A (as!n) b a ==>
               assertionsR Γ Θ Q A (AnnCall r n) (Call f) a" 
| AsSeqExpr1: "assertionsR Γ Θ (pre a2) A a1 c1 a ==>
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Seq c1 c2) a" 
| AsSeqExpr2: "assertionsR Γ Θ Q A a2 c2 a ==>
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Seq c1 c2) a" 
| AsCondExpr1: "assertionsR Γ Θ Q A a1 c1 a ==>
               assertionsR Γ Θ Q A (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AsCondExpr2: "assertionsR Γ Θ Q A a2 c2 a ==>
               assertionsR Γ Θ Q A (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AsCondAs: "assertionsR Γ Θ Q A (AnnBin r a1 a2) (Cond b c1 c2) r" 
| AsCatchExpr1: "assertionsR Γ Θ Q (pre a2) a1 c1 a ==>
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Catch c1 c2) a" 
| AsCatchExpr2: "assertionsR Γ Θ Q A a2 c2 a ==>
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Catch c1 c2) a" 

| AsParallelExprs: "i < length cs ==> assertionsR Γ Θ (postcond (as!i)) (abrcond (as!i)) (pres (as!i)) (cs!i) a ==>
    assertionsR Γ Θ Q A (AnnPar as) (Parallel cs) a" 
| AsParallelSkips: "Qs = ∩ (set (map postcond as)) ==>
  assertionsR Γ Θ Q A (AnnPar as) (Parallel cs) (Qs)" 

definition
  interfree_aux :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> 'f set ==> (('s,'p,'f) com × ('s, 'p, 'f) ann_triple × ('s,'p,'f) com × ('s, 'p, 'f) ann) ==> bool"
where
  "interfree_aux Γ Θ F ≡ λ(c₁, (P₁, Q₁, A₁), c₂, P₂).
                              (∀p c .atomicsR Γ Θ P₂ c₂ (p,c) ⟶
                               Γ⊨_F (Q₁ ∩ p) c Q₁,Q₁ ∧ Γ⊨_F (A₁ ∩ p) c A₁,A₁ ∧
                                (∀a. assertionsR Γ Θ Q₁ A₁ P₁ c₁ a ⟶ Γ⊨_F (a ∩ p) c a,a))"

definition
  interfree :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> 'f set ==> (('s, 'p, 'f) ann_triple) list ==> ('s,'p,'f) com list ==> bool"
where 
  "interfree Γ Θ F Ps Ts ≡ ∀i j. i < length Ts ∧ j < length Ts ∧ i ≠ j ⟶
                         interfree_aux Γ Θ F (Ts!i, Ps!i, Ts!j, fst (Ps!j))"

subsection ‹The Owicki-Gries Logic for COMPLX›

inductive
  oghoare :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> 'f set
              ==> ('s, 'p, 'f) ann ==> ('s,'p,'f) com ==> 's assn ==> 's assn ==> bool"
    (‹(4_, _/ ⊨_{/_} (_/ (_)/ _, _))› [60,60,60,1000,1000,1000,1000]60)
and
  oghoare_seq :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> 'f set
              ==> 's assn ==> ('s, 'p, 'f) ann ==> ('s,'p,'f) com ==> 's assn ==> 's assn ==> bool"
    (‹(4_, _/ ⊨!!!_{/_} (_/ _/ (_)/ _, _))› [60,60,60,1000,1000,1000,1000]60)

where
 Skip: " Γ, Θ ⊨_F (AnnExpr Q) Skip Q,A"

| Throw: "Γ, Θ ⊨_F (AnnExpr A) Throw Q,A"

| Basic: "Γ, Θ ⊨_F (AnnExpr {s. f s ∈ Q}) (Basic f) Q,A"

| Spec: "Γ, Θ ⊨_F (AnnExpr {s. (∀t. (s,t) ∈ rel ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ rel)}) (Spec rel) Q,A"

| Seq: "[Γ, Θ ⊨_F P₁ c₁ (pre P₂),A;
         Γ, Θ ⊨_F P₂ c₂ Q,A ]
         ==> Γ, Θ ⊨_F (AnnComp P₁ P₂) (Seq c₁ c₂) Q,A"

| Catch: "[Γ, Θ ⊨_F P₁ c₁ Q,(pre P₂);
           Γ, Θ ⊨_F P₂ c₂ Q,A ]
      ==> Γ, Θ ⊨_F (AnnComp P₁ P₂) (Catch c₁ c₂) Q,A"
  
| Cond: "[ Γ, Θ ⊨_F P₁ c₁ Q,A;
           Γ, Θ ⊨_F P₂ c₂ Q,A;
          r ∩ b ⊆ pre P₁;
          r ∩ -b ⊆ pre P₂ ]
         ==>
         Γ, Θ ⊨_F (AnnBin r P₁ P₂) (Cond b c₁ c₂) Q,A"

| While: "[ Γ, Θ ⊨_F P c i,A;
            i ∩ b ⊆ pre P;
            i ∩ -b ⊆ Q;
            r ⊆ i ]
          ==>
          Γ, Θ ⊨_F (AnnWhile r i P) (While b c) Q,A"

| Guard: "[ Γ, Θ ⊨_F P c Q,A;
            r ∩ g ⊆ pre P;
            r ∩ -g ≠ {} ⟶ f ∈ F] ==>
          Γ, Θ ⊨_F (AnnRec r P) (Guard f g c) Q,A"

| Call: "[ Θ p = Some as;
          (as ! n) = P;
          r ⊆ pre P;
          Γ p = Some b;
          n < length as;
          Γ,Θ ⊨_F P b Q,A
          ]
         ==>
         Γ, Θ ⊨_F (AnnCall r n) (Call p) Q,A"

| DynCom:
      "r ⊆ pre a ==> ∀s∈r. Γ, Θ ⊨_F a (c s) Q,A
      ==>
      Γ, Θ ⊨_F (AnnRec r a) (DynCom c) Q,A"

| Await: "[Γ, Θ ⊨!!!_F(r ∩ b) P c Q,A; atom_com c ] ==>
  Γ, Θ ⊨_F (AnnRec r P) (Await b c) Q,A"

| Parallel: "[ length as = length cs;
               ∀i < length cs. Γ,Θ⊨_F(pres (as!i)) (cs!i) (postcond (as!i)),(abrcond (as!i));
               interfree Γ Θ F as cs;
               ∩ (set (map postcond as)) ⊆ Q;
               ∪ (set (map abrcond as)) ⊆ A
              ]
        ==> Γ,Θ⊨_F (AnnPar as) (Parallel cs) Q,A"

| Conseq: "∃P' Q' A'. Γ,Θ⊨_F (weaken_pre P P') c Q',A' ∧ Q' ⊆ Q ∧ A' ⊆ A
           ==> Γ,Θ⊨_F P c Q,A"

| SeqSkip:   "Γ, Θ ⊨!!!_F Q (AnnExpr x) Skip Q,A"

| SeqThrow:   "Γ, Θ ⊨!!!_F A (AnnExpr x) Throw Q,A"

| SeqBasic:   "Γ, Θ ⊨!!!_F {s. f s ∈ Q} (AnnExpr x) (Basic f) Q,A"

| SeqSpec:   "Γ, Θ ⊨!!!_F {s. (∀t. (s,t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ r)} (AnnExpr x) (Spec r) Q,A"

| SeqSeq:    "[ Γ, Θ ⊨!!!_F R P₂ c₂ Q,A ; Γ, Θ ⊨!!!_F P P₁ c₁ R,A]
         ==> Γ, Θ ⊨!!!_F P (AnnComp P₁ P₂) (Seq c₁ c₂) Q,A"

| SeqCatch:  "[Γ, Θ ⊨!!!_F R P₂ c2 Q,A ; Γ, Θ ⊨!!!_F P P₁ c1 Q,R ] ==>
    Γ, Θ ⊨!!!_F P (AnnComp P₁ P₂) (Catch c1 c2) Q,A"

| SeqCond: "[ Γ, Θ ⊨!!!_F (P ∩ b) P₁ c₁ Q,A;
           Γ, Θ ⊨!!!_F (P ∩ -b) P₂ c₂ Q,A ]
         ==>
         Γ, Θ ⊨!!!_F P (AnnBin r P₁ P₂) (Cond b c₁ c₂) Q,A"

| SeqWhile: "[ Γ, Θ ⊨!!!_F (P∩b) a c P,A ]
          ==>
          Γ, Θ ⊨!!!_F P (AnnWhile r i a) (While b c) (P ∩ -b),A"

| SeqGuard: "[ Γ, Θ ⊨!!!_F (P∩g) a c Q,A;
            P ∩ -g ≠ {} ==> f ∈ F] ==>
          Γ, Θ ⊨!!!_F P (AnnRec r a) (Guard f g c) Q,A"

| SeqCall: "[ Θ p = Some as;
          (as ! n) = P'';
          Γ p = Some b;
          n < length as;
          Γ,Θ ⊨!!!_F P P'' b Q,A
          ]
         ==>
         Γ, Θ ⊨!!!_F P (AnnCall r n) (Call p) Q,A"

| SeqDynCom:
      "r ⊆ pre a ==>
      ∀s∈r. Γ, Θ ⊨!!!_FP a (c s) Q,A ==>
      P⊆r
      ==>
      Γ, Θ ⊨!!!_F P (AnnRec r a) (DynCom c) Q,A"

| SeqConseq: "[ P ⊆ P'; Γ,Θ⊨!!!_F P' a c Q',A'; Q' ⊆ Q; A' ⊆ A ]
           ==> Γ,Θ⊨!!!_F P a c Q,A"

| SeqParallel: "P ⊆ pre (AnnPar as) ==> Γ,Θ⊨_F (AnnPar as) (Parallel cs) Q,A
  ==> Γ,Θ⊨!!!_F P (AnnPar as) (Parallel cs) Q,A"

lemmas oghoare_intros = "oghoare_oghoare_seq.intros"

lemmas oghoare_inducts = oghoare_oghoare_seq.inducts

lemmas oghoare_induct = oghoare_oghoare_seq.inducts(1)

lemmas oghoare_seq_induct = oghoare_oghoare_seq.inducts(2)

end