Theory Annotate
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: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: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:T in D ⟧
⟹ P,E ⊢ e∙F{[]} ↝ e'∙F{D}"
| AnnoFAss: "⟦ P,E ⊢ e1 ↝ e1'; P,E ⊢ e2 ↝ e2';
P,E ⊢ e1' :: Class C; P ⊢ C sees F:T in D ⟧
⟹ P,E ⊢ e1∙F{[]} := e2 ↝ e1'∙F{D} := e2'"
| AnnoCall:
"⟦ P,E ⊢ e ↝ e'; P,E ⊢ es [↝] es' ⟧
⟹ P,E ⊢ Call e M es ↝ Call e' 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