Theory Annotate

(*  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 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,NonStatic: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,NonStatic:T in D 
    P,E  eF{[]}  e'F{D}"
| AnnoSFAcc:
  " P  C sees F,Static:T in D 
    P,E  CsF{[]}  CsF{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  e1F{[]} := e2  e1'F{D} := e2'"
| AnnoSFAss: " P,E  e2  e2'; P  C sees F,Static:T in D 
           P,E  CsF{[]} := e2  CsF{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