(* 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∙⇩_{s}F{[]} ↝ C∙⇩_{s}F{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∙⇩_{s}F{[]} := e2 ↝ C∙⇩_{s}F{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