Theory Annotate

(*  Title:      JinjaDCI/J/Annotate.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/Annotate.thy by Tobias Nipkow
*)

section ‹ Program annotation ›

theory Annotate imports WellType begin

(*<*)
abbreviation (output)
  unanFAcc :: "expr ⇒ vname ⇒ expr" ("(_∙_)" [10,10] 90) where
  "unanFAcc e F == FAcc e F []"

abbreviation (output)
  unanFAss :: "expr ⇒ vname ⇒ expr ⇒ expr" ("(_∙_ := _)" [10,0,90] 90) where
  "unanFAss e F e' == FAss e F [] e'"
(*>*)

inductive
  Anno :: "[J_prog,env, expr     , expr] ⇒ bool"
         ("_,_ ⊢ _ ↝ _"   [51,0,0,51]50)
  and Annos :: "[J_prog,env, expr list, expr list] ⇒ bool"
         ("_,_ ⊢ _ [↝] _" [51,0,0,51]50)
  for P :: J_prog
where
  
  AnnoNew: "P,E ⊢ new C ↝ new C"
| AnnoCast: "P,E ⊢ e ↝ e' ⟹ P,E ⊢ Cast C e ↝ Cast C e'"
| AnnoVal: "P,E ⊢ Val v ↝ Val v"
| AnnoVarVar: "E V = ⌊T⌋ ⟹ P,E ⊢ Var V ↝ Var V"
| AnnoVarField: "⟦ E V = None; E this = ⌊Class C⌋; P ⊢ C sees V,NonStatic:T in D ⟧
               ⟹ P,E ⊢ Var V ↝ Var this∙V{D}"
| AnnoBinOp:
  "⟦ P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2' ⟧
   ⟹ P,E ⊢ e1 «bop» e2 ↝ e1' «bop» e2'"
| AnnoLAssVar:
  "⟦ E V = ⌊T⌋; P,E ⊢ e ↝ e' ⟧ ⟹ P,E ⊢ V:=e ↝ V:=e'"
| AnnoLAssField:
  "⟦ E V = None; E this = ⌊Class C⌋; P ⊢ C sees V,NonStatic:T in D; P,E ⊢ e ↝ e' ⟧
   ⟹ P,E ⊢ V:=e ↝ Var this∙V{D} := e'"
| AnnoFAcc:
  "⟦ P,E ⊢ e ↝ e';  P,E ⊢ e' :: Class C;  P ⊢ C sees F,NonStatic:T in D ⟧
   ⟹ P,E ⊢ e∙F{[]} ↝ e'∙F{D}"
| AnnoSFAcc:
  "⟦ P ⊢ C sees F,Static:T in D ⟧
   ⟹ P,E ⊢ C∙⇩sF{[]} ↝ C∙⇩sF{D}"
| AnnoFAss: "⟦ P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2';
             P,E ⊢ e1' :: Class C; P ⊢ C sees F,NonStatic:T in D ⟧
          ⟹ P,E ⊢ e1∙F{[]} := e2 ↝ e1'∙F{D} := e2'"
| AnnoSFAss: "⟦ P,E ⊢ e2 ↝ e2'; P ⊢ C sees F,Static:T in D ⟧
          ⟹ P,E ⊢ C∙⇩sF{[]} := e2 ↝ C∙⇩sF{D} := e2'"
| AnnoCall:
  "⟦ P,E ⊢ e ↝ e';  P,E ⊢ es [↝] es' ⟧
   ⟹ P,E ⊢ Call e M es ↝ Call e' M es'"
| AnnoSCall:
  "⟦ P,E ⊢ es [↝] es' ⟧
   ⟹ P,E ⊢ SCall C M es ↝ SCall C M es'"
| AnnoBlock:
  "P,E(V ↦ T) ⊢ e ↝ e'  ⟹  P,E ⊢ {V:T; e} ↝ {V:T; e'}"
| AnnoComp: "⟦ P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2' ⟧
           ⟹  P,E ⊢ e1;;e2 ↝ e1';;e2'"
| AnnoCond: "⟦ P,E ⊢ e ↝ e'; P,E ⊢ e1 ↝ e1';  P,E ⊢ e2 ↝ e2' ⟧
          ⟹ P,E ⊢ if (e) e1 else e2 ↝ if (e') e1' else e2'"
| AnnoLoop: "⟦ P,E ⊢ e ↝ e';  P,E ⊢ c ↝ c' ⟧
          ⟹ P,E ⊢ while (e) c ↝ while (e') c'"
| AnnoThrow: "P,E ⊢ e ↝ e'  ⟹  P,E ⊢ throw e ↝ throw e'"
| AnnoTry: "⟦ P,E ⊢ e1 ↝ e1';  P,E(V ↦ Class C) ⊢ e2 ↝ e2' ⟧
         ⟹ P,E ⊢ try e1 catch(C V) e2 ↝ try e1' catch(C V) e2'"

| AnnoNil: "P,E ⊢ [] [↝] []"
| AnnoCons: "⟦ P,E ⊢ e ↝ e';  P,E ⊢ es [↝] es' ⟧
           ⟹  P,E ⊢ e#es [↝] e'#es'"

end