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