src/HOL/Bali/Term.thy
author wenzelm
Mon Jan 28 18:50:23 2002 +0100 (2002-01-28)
changeset 12857 a4386cc9b1c3
parent 12854 00d4a435777f
child 12858 6214f03d6d27
permissions -rw-r--r--
tuned header;
     1 (*  Title:      HOL/Bali/Term.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1997 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* Java expressions and statements *}
     8 
     9 theory Term = Value:
    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 datatype inv_mode                  (* invocation mode for method calls *)
    62 	= Static                   (* static *)
    63 	| SuperM                   (* super  *)
    64 	| IntVir                   (* interface or virtual *)
    65 
    66 record  sig =            (* signature of a method, cf. 8.4.2  *)
    67 	  name ::"mname"      (* acutally belongs to Decl.thy *)
    68           parTs::"ty list"        
    69 
    70 translations
    71   "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    72   "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    73 
    74 datatype jump
    75         = Break label (* break *)
    76         | Cont label  (* continue *)
    77         | Ret         (* return from method *)
    78 
    79 datatype var
    80 	= LVar                  lname(* local variable (incl. parameters) *)
    81         | FVar qtname bool expr vname(*class field*)("{_,_}_.._"[10,10,85,99]90)
    82 	| AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
    83 
    84 and expr
    85 	= NewC qtname              (* class instance creation *)
    86 	| NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
    87 	| Cast ty expr             (* type cast  *)
    88 	| Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
    89 	| Lit  val                 (* literal value, references not allowed *)
    90 	| Super                    (* special Super keyword *)
    91 	| Acc  var                 (* variable access *)
    92 	| Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
    93 	| Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
    94         | Call ref_ty inv_mode expr mname "(ty list)" (* method call *)
    95                   "(expr list)" ("{_,_}_\<cdot>_'( {_}_')"[10,10,85,99,10,10]85)
    96         | Methd qtname sig          (*   (folded) method (see below) *)
    97         | Body qtname stmt          (* (unfolded) method body *)
    98 and  stmt
    99 	= Skip                     (* empty      statement *)
   100 	| Expr  expr               (* expression statement *)
   101         | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   102                                    (* handles break *)
   103 	| Comp  stmt stmt          ("_;; _"                     [      66,65]65)
   104 	| If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
   105 	| Loop  label expr stmt    ("_\<bullet> While'(_') _"           [   99,80,79]70)
   106         | Do jump                  (* break, continue, return *)
   107 	| Throw expr
   108         | TryC  stmt
   109 	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   110 	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
   111 	| Init  qtname              (* class initialization *)
   112 
   113 
   114 text {*
   115 The expressions Methd and Body are artificial program constructs, in the
   116 sense that they are not used to define a concrete Bali program. In the 
   117 evaluation semantic definition they are "generated on the fly" to decompose 
   118 the task to define the behaviour of the Call expression. They are crucial 
   119 for the axiomatic semantics to give a syntactic hook to insert 
   120 some assertions (cf. AxSem.thy, Eval.thy).
   121 Also the Init statement (to initialize a class on its first use) is inserted 
   122 in various places by the evaluation semantics.   
   123 *}
   124  
   125 types "term" = "(expr+stmt, var, expr list) sum3"
   126 translations
   127   "sig"   <= (type) "mname \<times> ty list"
   128   "var"   <= (type) "Term.var"
   129   "expr"  <= (type) "Term.expr"
   130   "stmt"  <= (type) "Term.stmt"
   131   "term"  <= (type) "(expr+stmt, var, expr list) sum3"
   132 
   133 syntax
   134   
   135   this    :: expr
   136   LAcc    :: "vname \<Rightarrow>         expr" ("!!")
   137   LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
   138   Return  :: "expr \<Rightarrow> stmt"
   139   StatRef :: "ref_ty \<Rightarrow> expr"
   140 
   141 translations
   142   
   143  "this"       == "Acc (LVar This)"
   144  "!!v"        == "Acc (LVar (EName (VNam v)))"
   145  "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
   146  "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
   147                                                    (* Res := e;; Do Ret *)
   148  "StatRef rt" == "Cast (RefT rt) (Lit Null)"
   149   
   150 constdefs
   151 
   152   is_stmt :: "term \<Rightarrow> bool"
   153  "is_stmt t \<equiv> \<exists>c. t=In1r c"
   154 
   155 ML {*
   156 bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
   157 *}
   158 
   159 declare is_stmt_rews [simp]
   160 
   161 
   162 (* ############# Just testing syntax *)
   163 (** unfortunately cannot simply instantiate tnam **)
   164 (*
   165 datatype tnam_  = HasFoo_ | Base_ | Ext_
   166 datatype vnam_  = arr_ | vee_ | z_ | e_
   167 datatype label_ = lab1_
   168 
   169 consts
   170 
   171   tnam_ :: "tnam_  \<Rightarrow> tnam"
   172   vnam_ :: "vnam_  \<Rightarrow> vname"
   173   label_:: "label_ \<Rightarrow> label"
   174 axioms  
   175 
   176   inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
   177   inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
   178   inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
   179   
   180   
   181   surj_tnam_:  "\<exists>m. n = tnam_  m"
   182   surj_vnam_:  "\<exists>m. n = vnam_  m"
   183   surj_label_:" \<exists>m. n = label_ m"
   184 
   185 syntax
   186 
   187   HasFoo :: qtname
   188   Base   :: qtname
   189   Ext    :: qtname
   190   arr :: ename
   191   vee :: ename
   192   z   :: ename
   193   e   :: ename
   194   lab1:: label
   195 
   196 consts
   197   
   198   foo    :: mname
   199 translations
   200 
   201   "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
   202   "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
   203   "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
   204   "arr"    ==        "(vnam_ arr_)"
   205   "vee"    ==        "(vnam_ vee_)"
   206   "z"      ==        "(vnam_ z_)"
   207   "e"      ==        "(vnam_ e_)"
   208   "lab1"   ==        "label_ lab1_"
   209 
   210 constdefs test::stmt
   211 "test \<equiv>
   212 (lab1@ While(Acc  
   213       (Acc ({Base,True}StatRef (ClassT Object).arr).[Lit (Intg #2)])) Skip)"
   214 
   215 consts
   216  pTs :: "ty list"
   217    
   218 constdefs 
   219 
   220 test1::stmt
   221 "test1 \<equiv> 
   222   Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))"
   223 
   224 
   225 
   226 constdefs test::stmt
   227 "test \<equiv>
   228 (lab1\<cdot> While(Acc 
   229       (Acc ({Base,True}StatRef (ClassT Object)..arr).[Lit (Intg #2)])) Skip)"
   230 *)
   231 end