src/HOL/Bali/Term.thy
author schirmer
Fri Feb 22 11:26:44 2002 +0100 (2002-02-22)
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13337 f75dfc606ac7
permissions -rw-r--r--
Added check for field/method access to operational semantics and proved the acesses valid.
wenzelm@12857
     1
(*  Title:      HOL/Bali/Term.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
schirmer@12854
     7
header {* Java expressions and statements *}
schirmer@12854
     8
schirmer@12854
     9
theory Term = Value:
schirmer@12854
    10
schirmer@12854
    11
text {*
schirmer@12854
    12
design issues:
schirmer@12854
    13
\begin{itemize}
schirmer@12854
    14
\item invocation frames for local variables could be reduced to special static
schirmer@12854
    15
  objects (one per method). This would reduce redundancy, but yield a rather
schirmer@12854
    16
  non-standard execution model more difficult to understand.
schirmer@12854
    17
\item method bodies separated from calls to handle assumptions in axiomat. 
schirmer@12854
    18
  semantics
schirmer@12854
    19
  NB: Body is intended to be in the environment of the called method.
schirmer@12854
    20
\item class initialization is regarded as (auxiliary) statement 
schirmer@12854
    21
      (required for AxSem)
schirmer@12854
    22
\item result expression of method return is handled by a special result variable
schirmer@12854
    23
  result variable is treated uniformly with local variables
schirmer@12854
    24
  \begin{itemize}
schirmer@12854
    25
  \item[+] welltypedness and existence of the result/return expression is 
schirmer@12854
    26
           ensured without extra efford
schirmer@12854
    27
  \end{itemize}
schirmer@12854
    28
\end{itemize}
schirmer@12854
    29
schirmer@12854
    30
simplifications:
schirmer@12854
    31
\begin{itemize}
schirmer@12854
    32
\item expression statement allowed for any expression
schirmer@12854
    33
\item no unary, binary, etc, operators
schirmer@12854
    34
\item This  is modeled as a special non-assignable local variable
schirmer@12854
    35
\item Super is modeled as a general expression with the same value as This
schirmer@12854
    36
\item access to field x in current class via This.x
schirmer@12854
    37
\item NewA creates only one-dimensional arrays;
schirmer@12854
    38
  initialization of further subarrays may be simulated with nested NewAs
schirmer@12854
    39
\item The 'Lit' constructor is allowed to contain a reference value.
schirmer@12854
    40
  But this is assumed to be prohibited in the input language, which is enforced
schirmer@12854
    41
  by the type-checking rules.
schirmer@12854
    42
\item a call of a static method via a type name may be simulated by a dummy 
schirmer@12854
    43
      variable
schirmer@12854
    44
\item no nested blocks with inner local variables
schirmer@12854
    45
\item no synchronized statements
schirmer@12854
    46
\item no secondary forms of if, while (e.g. no for) (may be easily simulated)
schirmer@12854
    47
\item no switch (may be simulated with if)
schirmer@12854
    48
\item the @{text try_catch_finally} statement is divided into the 
schirmer@12854
    49
      @{text try_catch} statement 
schirmer@12854
    50
      and a finally statement, which may be considered as try..finally with 
schirmer@12854
    51
      empty catch
schirmer@12854
    52
\item the @{text try_catch} statement has exactly one catch clause; 
schirmer@12854
    53
      multiple ones can be
schirmer@12854
    54
  simulated with instanceof
schirmer@12854
    55
\item the compiler is supposed to add the annotations {@{text _}} during 
schirmer@12854
    56
      type-checking. This
schirmer@12854
    57
  transformation is left out as its result is checked by the type rules anyway
schirmer@12854
    58
\end{itemize}
schirmer@12854
    59
*}
schirmer@12854
    60
schirmer@12854
    61
datatype inv_mode                  (* invocation mode for method calls *)
schirmer@12854
    62
	= Static                   (* static *)
schirmer@12854
    63
	| SuperM                   (* super  *)
schirmer@12854
    64
	| IntVir                   (* interface or virtual *)
schirmer@12854
    65
schirmer@12854
    66
record  sig =            (* signature of a method, cf. 8.4.2  *)
schirmer@12854
    67
	  name ::"mname"      (* acutally belongs to Decl.thy *)
schirmer@12854
    68
          parTs::"ty list"        
schirmer@12854
    69
schirmer@12854
    70
translations
schirmer@12854
    71
  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
schirmer@12854
    72
  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
schirmer@12854
    73
schirmer@12854
    74
datatype jump
schirmer@12854
    75
        = Break label (* break *)
schirmer@12854
    76
        | Cont label  (* continue *)
schirmer@12854
    77
        | Ret         (* return from method *)
schirmer@12854
    78
schirmer@12854
    79
datatype var
schirmer@12854
    80
	= LVar                  lname(* local variable (incl. parameters) *)
schirmer@12925
    81
        | FVar qtname qtname bool expr vname
schirmer@12925
    82
                                (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
schirmer@12854
    83
	| AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
schirmer@12854
    84
schirmer@12854
    85
and expr
schirmer@12854
    86
	= NewC qtname              (* class instance creation *)
schirmer@12854
    87
	| NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
schirmer@12854
    88
	| Cast ty expr             (* type cast  *)
schirmer@12854
    89
	| Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
schirmer@12854
    90
	| Lit  val                 (* literal value, references not allowed *)
schirmer@12854
    91
	| Super                    (* special Super keyword *)
schirmer@12854
    92
	| Acc  var                 (* variable access *)
schirmer@12854
    93
	| Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
schirmer@12854
    94
	| Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
schirmer@12925
    95
        | Call qtname ref_ty inv_mode expr mname "(ty list)" (* method call *)
schirmer@12925
    96
                  "(expr list)" ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
schirmer@12854
    97
        | Methd qtname sig          (*   (folded) method (see below) *)
schirmer@12854
    98
        | Body qtname stmt          (* (unfolded) method body *)
schirmer@12854
    99
and  stmt
schirmer@12854
   100
	= Skip                     (* empty      statement *)
schirmer@12854
   101
	| Expr  expr               (* expression statement *)
schirmer@12854
   102
        | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
schirmer@12854
   103
                                   (* handles break *)
schirmer@12854
   104
	| Comp  stmt stmt          ("_;; _"                     [      66,65]65)
schirmer@12854
   105
	| If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
schirmer@12854
   106
	| Loop  label expr stmt    ("_\<bullet> While'(_') _"           [   99,80,79]70)
schirmer@12854
   107
        | Do jump                  (* break, continue, return *)
schirmer@12854
   108
	| Throw expr
schirmer@12854
   109
        | TryC  stmt
schirmer@12854
   110
	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
schirmer@12854
   111
	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
schirmer@12854
   112
	| Init  qtname              (* class initialization *)
schirmer@12854
   113
schirmer@12854
   114
schirmer@12854
   115
text {*
schirmer@12854
   116
The expressions Methd and Body are artificial program constructs, in the
schirmer@12854
   117
sense that they are not used to define a concrete Bali program. In the 
schirmer@12854
   118
evaluation semantic definition they are "generated on the fly" to decompose 
schirmer@12854
   119
the task to define the behaviour of the Call expression. They are crucial 
schirmer@12854
   120
for the axiomatic semantics to give a syntactic hook to insert 
schirmer@12854
   121
some assertions (cf. AxSem.thy, Eval.thy).
schirmer@12854
   122
Also the Init statement (to initialize a class on its first use) is inserted 
schirmer@12854
   123
in various places by the evaluation semantics.   
schirmer@12854
   124
*}
schirmer@12854
   125
 
schirmer@12854
   126
types "term" = "(expr+stmt, var, expr list) sum3"
schirmer@12854
   127
translations
schirmer@12854
   128
  "sig"   <= (type) "mname \<times> ty list"
schirmer@12854
   129
  "var"   <= (type) "Term.var"
schirmer@12854
   130
  "expr"  <= (type) "Term.expr"
schirmer@12854
   131
  "stmt"  <= (type) "Term.stmt"
schirmer@12854
   132
  "term"  <= (type) "(expr+stmt, var, expr list) sum3"
schirmer@12854
   133
schirmer@12854
   134
syntax
schirmer@12854
   135
  
schirmer@12854
   136
  this    :: expr
schirmer@12854
   137
  LAcc    :: "vname \<Rightarrow>         expr" ("!!")
schirmer@12854
   138
  LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
schirmer@12854
   139
  Return  :: "expr \<Rightarrow> stmt"
schirmer@12854
   140
  StatRef :: "ref_ty \<Rightarrow> expr"
schirmer@12854
   141
schirmer@12854
   142
translations
schirmer@12854
   143
  
schirmer@12854
   144
 "this"       == "Acc (LVar This)"
schirmer@12854
   145
 "!!v"        == "Acc (LVar (EName (VNam v)))"
schirmer@12854
   146
 "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
schirmer@12854
   147
 "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
schirmer@12854
   148
                                                   (* Res := e;; Do Ret *)
schirmer@12854
   149
 "StatRef rt" == "Cast (RefT rt) (Lit Null)"
schirmer@12854
   150
  
schirmer@12854
   151
constdefs
schirmer@12854
   152
schirmer@12854
   153
  is_stmt :: "term \<Rightarrow> bool"
schirmer@12854
   154
 "is_stmt t \<equiv> \<exists>c. t=In1r c"
schirmer@12854
   155
schirmer@12854
   156
ML {*
schirmer@12854
   157
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
schirmer@12854
   158
*}
schirmer@12854
   159
schirmer@12854
   160
declare is_stmt_rews [simp]
schirmer@12854
   161
end