src/HOL/Bali/Term.thy
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13345 bd611943cbc2
     1.1 --- a/src/HOL/Bali/Term.thy	Wed Jul 10 14:51:18 2002 +0200
     1.2 +++ b/src/HOL/Bali/Term.thy	Wed Jul 10 15:07:02 2002 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  header {* Java expressions and statements *}
     1.6  
     1.7 -theory Term = Value:
     1.8 +theory Term = Value + Table:
     1.9  
    1.10  text {*
    1.11  design issues:
    1.12 @@ -58,6 +58,40 @@
    1.13  \end{itemize}
    1.14  *}
    1.15  
    1.16 +
    1.17 +
    1.18 +types locals = "(lname, val) table"  (* local variables *)
    1.19 +
    1.20 +
    1.21 +datatype jump
    1.22 +        = Break label (* break *)
    1.23 +        | Cont label  (* continue *)
    1.24 +        | Ret         (* return from method *)
    1.25 +
    1.26 +datatype xcpt        (* exception *)
    1.27 +	= Loc loc    (* location of allocated execption object *)
    1.28 +	| Std xname  (* intermediate standard exception, see Eval.thy *)
    1.29 +
    1.30 +datatype error
    1.31 +       = AccessViolation (* Access to a member that isn't permitted *)
    1.32 +
    1.33 +datatype abrupt      (* abrupt completion *) 
    1.34 +        = Xcpt xcpt  (* exception *)
    1.35 +        | Jump jump  (* break, continue, return *)
    1.36 +        | Error error (* runtime errors, we wan't to detect and proof absent
    1.37 +                         in welltyped programms *)
    1.38 +types
    1.39 +  abopt  = "abrupt option"
    1.40 +
    1.41 +text {* Local variable store and exception. 
    1.42 +Anticipation of State.thy used by smallstep semantics. For a method call, 
    1.43 +we save the local variables of the caller in the term Callee to restore them 
    1.44 +after method return. Also an exception must be restored after the finally
    1.45 +statement *}
    1.46 +
    1.47 +translations
    1.48 + "locals" <= (type) "(lname, val) table"
    1.49 +
    1.50  datatype inv_mode                  (* invocation mode for method calls *)
    1.51  	= Static                   (* static *)
    1.52  	| SuperM                   (* super  *)
    1.53 @@ -71,71 +105,112 @@
    1.54    "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    1.55    "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    1.56  
    1.57 -datatype jump
    1.58 -        = Break label (* break *)
    1.59 -        | Cont label  (* continue *)
    1.60 -        | Ret         (* return from method *)
    1.61 +-- "function codes for unary operations"
    1.62 +datatype unop =  UPlus    -- "+ unary plus" 
    1.63 +               | UMinus   -- "- unary minus"
    1.64 +               | UBitNot  -- "~ bitwise NOT"
    1.65 +               | UNot     -- "! logical complement"
    1.66 +
    1.67 +-- "function codes for binary operations"
    1.68 +datatype binop = Mul     -- "*   multiplication"
    1.69 +               | Div     -- "/   division"
    1.70 +               | Mod     -- "%   remainder"
    1.71 +               | Plus    -- "+   addition"
    1.72 +               | Minus   -- "-   subtraction"
    1.73 +               | LShift  -- "<<  left shift"
    1.74 +               | RShift  -- ">>  signed right shift"
    1.75 +               | RShiftU -- ">>> unsigned right shift"
    1.76 +               | Less    -- "<   less than"
    1.77 +               | Le      -- "<=  less than or equal"
    1.78 +               | Greater -- ">   greater than"
    1.79 +               | Ge      -- ">=  greater than or equal"
    1.80 +               | Eq      -- "==  equal"
    1.81 +               | Neq     -- "!=  not equal"
    1.82 +               | BitAnd  -- "&   bitwise AND"
    1.83 +               | And     -- "&   boolean AND"
    1.84 +               | BitXor  -- "^   bitwise Xor"
    1.85 +               | Xor     -- "^   boolean Xor"
    1.86 +               | BitOr   -- "|   bitwise Or"
    1.87 +               | Or      -- "|   boolean Or"
    1.88  
    1.89  datatype var
    1.90  	= LVar                  lname(* local variable (incl. parameters) *)
    1.91          | FVar qtname qtname bool expr vname
    1.92                                  (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
    1.93 -	| AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
    1.94 +	| AVar expr expr    (* array component *) ("_.[_]"[90,10   ]90)
    1.95 +        | InsInitV stmt var (* insertion of initialization before
    1.96 +                                   evaluation of var (for smallstep sem.) *)
    1.97  
    1.98  and expr
    1.99 -	= NewC qtname              (* class instance creation *)
   1.100 -	| NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
   1.101 -	| Cast ty expr             (* type cast  *)
   1.102 -	| Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
   1.103 -	| Lit  val                 (* literal value, references not allowed *)
   1.104 -	| Super                    (* special Super keyword *)
   1.105 -	| Acc  var                 (* variable access *)
   1.106 -	| Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
   1.107 -	| Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
   1.108 -        | Call qtname ref_ty inv_mode expr mname "(ty list)" (* method call *)
   1.109 -                  "(expr list)" ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
   1.110 -        | Methd qtname sig          (*   (folded) method (see below) *)
   1.111 -        | Body qtname stmt          (* (unfolded) method body *)
   1.112 +	= NewC qtname         (* class instance creation *)
   1.113 +	| NewA ty expr        (* array creation *) ("New _[_]"[99,10   ]85)
   1.114 +	| Cast ty expr        (* type cast  *)
   1.115 +	| Inst expr ref_ty    (* instanceof *)     ("_ InstOf _"[85,99] 85)
   1.116 +	| Lit  val            (* literal value, references not allowed *)
   1.117 +        | UnOp unop expr        (* unary operation *)
   1.118 +        | BinOp binop expr expr (* binary operation *)
   1.119 +        
   1.120 +	| Super               (* special Super keyword *)
   1.121 +	| Acc  var            (* variable access *)
   1.122 +	| Ass  var expr       (* variable assign *) ("_:=_"   [90,85   ]85)
   1.123 +	| Cond expr expr expr (* conditional *)  ("_ ? _ : _" [85,85,80]80)
   1.124 +        | Call qtname ref_ty inv_mode expr mname "(ty list)" 
   1.125 +               "(expr list)"  (* method call *) 
   1.126 +                              ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
   1.127 +        | Methd qtname sig    (*   (folded) method (see below) *)
   1.128 +        | Body qtname stmt    (* (unfolded) method body *)
   1.129 +        | InsInitE stmt expr      (* insertion of initialization before
   1.130 +                                   evaluation of expr (for smallstep sem.) *)
   1.131 +        | Callee locals expr      (* save Callers locals in Callee-Frame
   1.132 +                                     (for smallstep semantics) *)
   1.133  and  stmt
   1.134 -	= Skip                     (* empty      statement *)
   1.135 -	| Expr  expr               (* expression statement *)
   1.136 -        | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   1.137 -                                   (* handles break *)
   1.138 -	| Comp  stmt stmt          ("_;; _"                     [      66,65]65)
   1.139 -	| If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
   1.140 -	| Loop  label expr stmt    ("_\<bullet> While'(_') _"           [   99,80,79]70)
   1.141 -        | Do jump                  (* break, continue, return *)
   1.142 +	= Skip                  (* empty      statement *)
   1.143 +	| Expr  expr            (* expression statement *)
   1.144 +        | Lab   jump stmt       ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   1.145 +                                (* handles break *)
   1.146 +	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
   1.147 +	| If_   expr stmt stmt  ("If'(_') _ Else _"          [   80,79,79]70)
   1.148 +	| Loop  label expr stmt ("_\<bullet> While'(_') _"           [   99,80,79]70)
   1.149 +        | Do jump               (* break, continue, return *)
   1.150  	| Throw expr
   1.151          | TryC  stmt
   1.152 -	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   1.153 -	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
   1.154 +	     qtname vname stmt ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   1.155 +	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   1.156 +        | FinA abopt stmt        (* Save abruption of first statement 
   1.157 +                                    (for smallstep sem.) *)
   1.158  	| Init  qtname              (* class initialization *)
   1.159  
   1.160  
   1.161  text {*
   1.162  The expressions Methd and Body are artificial program constructs, in the
   1.163  sense that they are not used to define a concrete Bali program. In the 
   1.164 -evaluation semantic definition they are "generated on the fly" to decompose 
   1.165 -the task to define the behaviour of the Call expression. They are crucial 
   1.166 -for the axiomatic semantics to give a syntactic hook to insert 
   1.167 -some assertions (cf. AxSem.thy, Eval.thy).
   1.168 -Also the Init statement (to initialize a class on its first use) is inserted 
   1.169 -in various places by the evaluation semantics.   
   1.170 +operational semantic's they are "generated on the fly" 
   1.171 +to decompose the task to define the behaviour of the Call expression. 
   1.172 +They are crucial for the axiomatic semantics to give a syntactic hook to insert 
   1.173 +some assertions (cf. AxSem.thy, Eval.thy). 
   1.174 +The Init statement (to initialize a class on its first use) is 
   1.175 +inserted in various places by the semantics. 
   1.176 +Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
   1.177 +smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
   1.178 +local variables of the caller for method return. So ve avoid modelling a 
   1.179 +frame stack.
   1.180 +The InsInitV/E terms are only used by the smallstep semantics to model the
   1.181 +intermediate steps of class-initialisation.
   1.182  *}
   1.183   
   1.184 -types "term" = "(expr+stmt, var, expr list) sum3"
   1.185 +types "term" = "(expr+stmt,var,expr list) sum3"
   1.186  translations
   1.187    "sig"   <= (type) "mname \<times> ty list"
   1.188    "var"   <= (type) "Term.var"
   1.189    "expr"  <= (type) "Term.expr"
   1.190    "stmt"  <= (type) "Term.stmt"
   1.191 -  "term"  <= (type) "(expr+stmt, var, expr list) sum3"
   1.192 +  "term"  <= (type) "(expr+stmt,var,expr list) sum3"
   1.193  
   1.194  syntax
   1.195    
   1.196    this    :: expr
   1.197 -  LAcc    :: "vname \<Rightarrow>         expr" ("!!")
   1.198 -  LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
   1.199 +  LAcc    :: "vname \<Rightarrow> expr" ("!!")
   1.200 +  LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   1.201    Return  :: "expr \<Rightarrow> stmt"
   1.202    StatRef :: "ref_ty \<Rightarrow> expr"
   1.203