header {* \isaheader{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"
("_,_ \<turnstile> _ \<leadsto> _" [51,0,0,51]50)
and Annos :: "[J_prog,env, expr list, expr list] => bool"
("_,_ \<turnstile> _ [\<leadsto>] _" [51,0,0,51]50)
for P :: J_prog
where
AnnoNew: "P,E \<turnstile> new C \<leadsto> new C"
| AnnoCast: "P,E \<turnstile> e \<leadsto> e' ==> P,E \<turnstile> Cast C e \<leadsto> Cast C e'"
| AnnoVal: "P,E \<turnstile> Val v \<leadsto> Val v"
| AnnoVarVar: "E V = ⌊T⌋ ==> P,E \<turnstile> Var V \<leadsto> Var V"
| AnnoVarField: "[| E V = None; E this = ⌊Class C⌋; P \<turnstile> C sees V:T in D |]
==> P,E \<turnstile> Var V \<leadsto> Var this•V{D}"
| AnnoBinOp:
"[| P,E \<turnstile> e1 \<leadsto> e1'; P,E \<turnstile> e2 \<leadsto> e2' |]
==> P,E \<turnstile> e1 «bop» e2 \<leadsto> e1' «bop» e2'"
| AnnoLAssVar:
"[| E V = ⌊T⌋; P,E \<turnstile> e \<leadsto> e' |] ==> P,E \<turnstile> V:=e \<leadsto> V:=e'"
| AnnoLAssField:
"[| E V = None; E this = ⌊Class C⌋; P \<turnstile> C sees V:T in D; P,E \<turnstile> e \<leadsto> e' |]
==> P,E \<turnstile> V:=e \<leadsto> Var this•V{D} := e'"
| AnnoFAcc:
"[| P,E \<turnstile> e \<leadsto> e'; P,E \<turnstile> e' :: Class C; P \<turnstile> C sees F:T in D |]
==> P,E \<turnstile> e•F{[]} \<leadsto> e'•F{D}"
| AnnoFAss: "[| P,E \<turnstile> e1 \<leadsto> e1'; P,E \<turnstile> e2 \<leadsto> e2';
P,E \<turnstile> e1' :: Class C; P \<turnstile> C sees F:T in D |]
==> P,E \<turnstile> e1•F{[]} := e2 \<leadsto> e1'•F{D} := e2'"
| AnnoCall:
"[| P,E \<turnstile> e \<leadsto> e'; P,E \<turnstile> es [\<leadsto>] es' |]
==> P,E \<turnstile> Call e M es \<leadsto> Call e' M es'"
| AnnoBlock:
"P,E(V \<mapsto> T) \<turnstile> e \<leadsto> e' ==> P,E \<turnstile> {V:T; e} \<leadsto> {V:T; e'}"
| AnnoComp: "[| P,E \<turnstile> e1 \<leadsto> e1'; P,E \<turnstile> e2 \<leadsto> e2' |]
==> P,E \<turnstile> e1;;e2 \<leadsto> e1';;e2'"
| AnnoCond: "[| P,E \<turnstile> e \<leadsto> e'; P,E \<turnstile> e1 \<leadsto> e1'; P,E \<turnstile> e2 \<leadsto> e2' |]
==> P,E \<turnstile> if (e) e1 else e2 \<leadsto> if (e') e1' else e2'"
| AnnoLoop: "[| P,E \<turnstile> e \<leadsto> e'; P,E \<turnstile> c \<leadsto> c' |]
==> P,E \<turnstile> while (e) c \<leadsto> while (e') c'"
| AnnoThrow: "P,E \<turnstile> e \<leadsto> e' ==> P,E \<turnstile> throw e \<leadsto> throw e'"
| AnnoTry: "[| P,E \<turnstile> e1 \<leadsto> e1'; P,E(V \<mapsto> Class C) \<turnstile> e2 \<leadsto> e2' |]
==> P,E \<turnstile> try e1 catch(C V) e2 \<leadsto> try e1' catch(C V) e2'"
| AnnoNil: "P,E \<turnstile> [] [\<leadsto>] []"
| AnnoCons: "[| P,E \<turnstile> e \<leadsto> e'; P,E \<turnstile> es [\<leadsto>] es' |]
==> P,E \<turnstile> e#es [\<leadsto>] e'#es'"
end