Theory Annotate

(*  Title:      Jinja/J/Annotate.thy
    ID:         $Id: Annotate.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Program annotation} *}

theory Annotate = WellType:

(*<*)
syntax (output)
  unanFAcc :: "expr => vname => expr" ("(_\<bullet>_)" [10,10] 90)
  unanFAss :: "expr => vname => expr => expr" ("(_\<bullet>_ := _)" [10,0,90] 90)

translations
  "unanFAcc e F" == "FAcc e F []"
  "unanFAss e F e'" == "FAss e F [] e'"
(*>*)

consts
  Anno :: "J_prog => (env × expr      × expr) set"
  Annos:: "J_prog => (env × expr list × expr list) set"

(*<*)
syntax (xsymbols)
  Anno :: "[J_prog,env, expr     , expr] => bool"
         ("_,_ \<turnstile> _ \<leadsto> _"   [51,0,0,51]50)
  Annos:: "[J_prog,env, expr list, expr list] => bool"
         ("_,_ \<turnstile> _ [\<leadsto>] _" [51,0,0,51]50)
(*>*)

translations
  "P,E \<turnstile> e \<leadsto> e'" == "(E,e,e') ∈ Anno P"
  "P,E \<turnstile> es [\<leadsto>] es'" == "(E,es,es') ∈ Annos P"

inductive "Anno P" "Annos P"
intros
  
AnnoNew: "is_class P C  ==>  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\<bullet>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'"
AnnoLAss:
  "P,E \<turnstile> e \<leadsto> e' ==> P,E \<turnstile> V:=e \<leadsto> V:=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\<bullet>F{[]} \<leadsto> e'\<bullet>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\<bullet>F{[]} := e2 \<leadsto> e1'\<bullet>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