src/HOL/Bali/Term.thy
author schirmer
Mon Jul 15 10:41:34 2002 +0200 (2002-07-15)
changeset 13358 c837ba4cfb62
parent 13345 bd611943cbc2
child 13384 a34e38154413
permissions -rw-r--r--
fix latex output
     1 (*  Title:      HOL/Bali/Term.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Java expressions and statements *}
     8 
     9 theory Term = Value + Table:
    10 
    11 text {*
    12 design issues:
    13 \begin{itemize}
    14 \item invocation frames for local variables could be reduced to special static
    15   objects (one per method). This would reduce redundancy, but yield a rather
    16   non-standard execution model more difficult to understand.
    17 \item method bodies separated from calls to handle assumptions in axiomat. 
    18   semantics
    19   NB: Body is intended to be in the environment of the called method.
    20 \item class initialization is regarded as (auxiliary) statement 
    21       (required for AxSem)
    22 \item result expression of method return is handled by a special result variable
    23   result variable is treated uniformly with local variables
    24   \begin{itemize}
    25   \item[+] welltypedness and existence of the result/return expression is 
    26            ensured without extra efford
    27   \end{itemize}
    28 \end{itemize}
    29 
    30 simplifications:
    31 \begin{itemize}
    32 \item expression statement allowed for any expression
    33 \item no unary, binary, etc, operators
    34 \item This  is modeled as a special non-assignable local variable
    35 \item Super is modeled as a general expression with the same value as This
    36 \item access to field x in current class via This.x
    37 \item NewA creates only one-dimensional arrays;
    38   initialization of further subarrays may be simulated with nested NewAs
    39 \item The 'Lit' constructor is allowed to contain a reference value.
    40   But this is assumed to be prohibited in the input language, which is enforced
    41   by the type-checking rules.
    42 \item a call of a static method via a type name may be simulated by a dummy 
    43       variable
    44 \item no nested blocks with inner local variables
    45 \item no synchronized statements
    46 \item no secondary forms of if, while (e.g. no for) (may be easily simulated)
    47 \item no switch (may be simulated with if)
    48 \item the @{text try_catch_finally} statement is divided into the 
    49       @{text try_catch} statement 
    50       and a finally statement, which may be considered as try..finally with 
    51       empty catch
    52 \item the @{text try_catch} statement has exactly one catch clause; 
    53       multiple ones can be
    54   simulated with instanceof
    55 \item the compiler is supposed to add the annotations {@{text _}} during 
    56       type-checking. This
    57   transformation is left out as its result is checked by the type rules anyway
    58 \end{itemize}
    59 *}
    60 
    61 
    62 
    63 types locals = "(lname, val) table"  (* local variables *)
    64 
    65 
    66 datatype jump
    67         = Break label (* break *)
    68         | Cont label  (* continue *)
    69         | Ret         (* return from method *)
    70 
    71 datatype xcpt        (* exception *)
    72 	= Loc loc    (* location of allocated execption object *)
    73 	| Std xname  (* intermediate standard exception, see Eval.thy *)
    74 
    75 datatype error
    76        = AccessViolation (* Access to a member that isn't permitted *)
    77 
    78 datatype abrupt      (* abrupt completion *) 
    79         = Xcpt xcpt  (* exception *)
    80         | Jump jump  (* break, continue, return *)
    81         | Error error (* runtime errors, we wan't to detect and proof absent
    82                          in welltyped programms *)
    83 types
    84   abopt  = "abrupt option"
    85 
    86 text {* Local variable store and exception. 
    87 Anticipation of State.thy used by smallstep semantics. For a method call, 
    88 we save the local variables of the caller in the term Callee to restore them 
    89 after method return. Also an exception must be restored after the finally
    90 statement *}
    91 
    92 translations
    93  "locals" <= (type) "(lname, val) table"
    94 
    95 datatype inv_mode                  (* invocation mode for method calls *)
    96 	= Static                   (* static *)
    97 	| SuperM                   (* super  *)
    98 	| IntVir                   (* interface or virtual *)
    99 
   100 record  sig =            (* signature of a method, cf. 8.4.2  *)
   101 	  name ::"mname"      (* acutally belongs to Decl.thy *)
   102           parTs::"ty list"        
   103 
   104 translations
   105   "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
   106   "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
   107 
   108 -- "function codes for unary operations"
   109 datatype unop =  UPlus    
   110                | UMinus   
   111                | UBitNot  
   112                | UNot     
   113 
   114 -- "function codes for binary operations"
   115 datatype binop = Mul     
   116                | Div     
   117                | Mod     
   118                | Plus    
   119                | Minus   
   120                | LShift  
   121                | RShift  
   122                | RShiftU 
   123                | Less    
   124                | Le      
   125                | Greater 
   126                | Ge      
   127                | Eq      
   128                | Neq     
   129                | BitAnd  
   130                | And     
   131                | BitXor  
   132                | Xor     
   133                | BitOr   
   134                | Or      
   135 
   136 datatype var
   137 	= LVar                  lname(* local variable (incl. parameters) *)
   138         | FVar qtname qtname bool expr vname
   139                                 (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
   140 	| AVar expr expr    (* array component *) ("_.[_]"[90,10   ]90)
   141         | InsInitV stmt var (* insertion of initialization before
   142                                    evaluation of var (for smallstep sem.) *)
   143 
   144 and expr
   145 	= NewC qtname         (* class instance creation *)
   146 	| NewA ty expr        (* array creation *) ("New _[_]"[99,10   ]85)
   147 	| Cast ty expr        (* type cast  *)
   148 	| Inst expr ref_ty    (* instanceof *)     ("_ InstOf _"[85,99] 85)
   149 	| Lit  val            (* literal value, references not allowed *)
   150         | UnOp unop expr        (* unary operation *)
   151         | BinOp binop expr expr (* binary operation *)
   152         
   153 	| Super               (* special Super keyword *)
   154 	| Acc  var            (* variable access *)
   155 	| Ass  var expr       (* variable assign *) ("_:=_"   [90,85   ]85)
   156 	| Cond expr expr expr (* conditional *)  ("_ ? _ : _" [85,85,80]80)
   157         | Call qtname ref_ty inv_mode expr mname "(ty list)" 
   158                "(expr list)"  (* method call *) 
   159                               ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
   160         | Methd qtname sig    (*   (folded) method (see below) *)
   161         | Body qtname stmt    (* (unfolded) method body *)
   162         | InsInitE stmt expr      (* insertion of initialization before
   163                                    evaluation of expr (for smallstep sem.) *)
   164         | Callee locals expr      (* save Callers locals in Callee-Frame
   165                                      (for smallstep semantics) *)
   166 and  stmt
   167 	= Skip                  (* empty      statement *)
   168 	| Expr  expr            (* expression statement *)
   169         | Lab   jump stmt       ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   170                                 (* handles break *)
   171 	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
   172 	| If_   expr stmt stmt  ("If'(_') _ Else _"          [   80,79,79]70)
   173 	| Loop  label expr stmt ("_\<bullet> While'(_') _"           [   99,80,79]70)
   174         | Do jump               (* break, continue, return *)
   175 	| Throw expr
   176         | TryC  stmt
   177 	     qtname vname stmt ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   178 	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   179         | FinA abopt stmt        (* Save abruption of first statement 
   180                                     (for smallstep sem.) *)
   181 	| Init  qtname              (* class initialization *)
   182 
   183 
   184 text {*
   185 The expressions Methd and Body are artificial program constructs, in the
   186 sense that they are not used to define a concrete Bali program. In the 
   187 operational semantic's they are "generated on the fly" 
   188 to decompose the task to define the behaviour of the Call expression. 
   189 They are crucial for the axiomatic semantics to give a syntactic hook to insert 
   190 some assertions (cf. AxSem.thy, Eval.thy). 
   191 The Init statement (to initialize a class on its first use) is 
   192 inserted in various places by the semantics. 
   193 Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
   194 smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
   195 local variables of the caller for method return. So ve avoid modelling a 
   196 frame stack.
   197 The InsInitV/E terms are only used by the smallstep semantics to model the
   198 intermediate steps of class-initialisation.
   199 *}
   200  
   201 types "term" = "(expr+stmt,var,expr list) sum3"
   202 translations
   203   "sig"   <= (type) "mname \<times> ty list"
   204   "var"   <= (type) "Term.var"
   205   "expr"  <= (type) "Term.expr"
   206   "stmt"  <= (type) "Term.stmt"
   207   "term"  <= (type) "(expr+stmt,var,expr list) sum3"
   208 
   209 syntax
   210   
   211   this    :: expr
   212   LAcc    :: "vname \<Rightarrow> expr" ("!!")
   213   LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   214   Return  :: "expr \<Rightarrow> stmt"
   215   StatRef :: "ref_ty \<Rightarrow> expr"
   216 
   217 translations
   218   
   219  "this"       == "Acc (LVar This)"
   220  "!!v"        == "Acc (LVar (EName (VNam v)))"
   221  "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
   222  "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
   223                                                    (* Res := e;; Do Ret *)
   224  "StatRef rt" == "Cast (RefT rt) (Lit Null)"
   225   
   226 constdefs
   227 
   228   is_stmt :: "term \<Rightarrow> bool"
   229  "is_stmt t \<equiv> \<exists>c. t=In1r c"
   230 
   231 ML {*
   232 bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
   233 *}
   234 
   235 declare is_stmt_rews [simp]
   236 
   237 axclass inj_term < "type"
   238 consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
   239 
   240 instance stmt::inj_term ..
   241 
   242 defs (overloaded)
   243 stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
   244 
   245 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
   246 by (simp add: stmt_inj_term_def)
   247 
   248 instance expr::inj_term ..
   249 
   250 defs (overloaded)
   251 expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
   252 
   253 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
   254 by (simp add: expr_inj_term_def)
   255 
   256 instance var::inj_term ..
   257 
   258 defs (overloaded)
   259 var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
   260 
   261 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
   262 by (simp add: var_inj_term_def)
   263 
   264 instance "list":: (type) inj_term ..
   265 
   266 defs (overloaded)
   267 expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   268 
   269 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   270 by (simp add: expr_list_inj_term_def)
   271 
   272 end