Theory Annotate

(*  Title:      Jinja/J/Annotate.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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 thisV{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 thisV{D} := e'"
| AnnoFAcc:
  " P,E  e  e';  P,E  e' :: Class C;  P  C sees F:T in D 
    P,E  eF{[]}  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  e1F{[]} := 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