Theory Term

Up to index of Isabelle/Bali4

(*  Title:      isabelle/Bali/Term.thy
    ID:         $Id: Term.thy,v 1.41 2000/08/07 21:07:49 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Java expressions and statements

design issues:
* invocation frames for local variables could be reduced to special static
  objects (one per method). This would reduce redundancy, but yield a rather
  non-standard execution model more difficult to understand.
* method bodies separated from calls to handle assumptions in axiomat. semantics
  NB: Body is intended to be in the environment of the _called_ method.
* class initialization is regarded as (auxiliary) statement (required for AxSem)
simplifications:
* expression statement allowed for any expression
* no unary, binary, etc, operators
* This  is modeled as a special non-assignable local variable
* Super is modeled as a general expression with the same value as This
* access to field x in current class via This.x
* NewA creates only one-dimensional arrays;
  initialization of further subarrays may be simulated with nested NewAs
* The 'Lit' constructor is allowed to contain a reference value.
  But this is assumed to be prohibited in the input language, which is enforced
  by the type-checking rules.
* a call of a static method via a type name may be simulated by a dummy variable
* result expression instead of return statement (see Decl.thy)
* no nested blocks with inner local variables
* no synchronized statements
* no secondary forms of if, while (e.g. no for) (may be easily simulated)
* no switch, break, continue, no labels (may be simulated with while)
* the try_catch_finally statement is divided into the try_catch statement and
  a finally statement, which may be considered as try..finally with empty catch
* the try_catch statement has exactly one catch clause; multiple ones can be
  simulated with instanceof
* the compiler is supposed to add the annotations {_} during type-checking. This
  transformation is left out as its result is checked by the type rules anyway
*)
Term = Value + 

datatype inv_mode                  (* invocation mode for method calls *)
        = Static                   (* static *)
        | SuperM                   (* super  *)
        | IntVir                   (* interface or virtual *)

types    sig             (* signature of a method, cf. 8.4.2  *)
        = "mname × ty list"        (* acutally belongs to Decl.thy *)

datatype var
        = LVar                  lname(* local variable (incl. parameters) *)
        | FVar  tname bool expr ename(*class field*)("{_,_}_.._"[10,10,85,99]90)
        | AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
and expr
        = NewC tname               (* class instance creation *)
        | NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
        | Cast ty expr             (* type cast  *)
        | Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
        | Lit  val                 (* literal value, references not allowed *)
        | Super                    (* special Super keyword *)
        | Acc  var                 (* variable access *)
        | Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
        | Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
        | Call ref_ty ref_ty inv_mode expr mname (* method call *)
          (ty list) (expr list) ("{_,_,_}_.._'( {_}_')"[10,10,10,85,99,10,10]85)
        | Methd tname sig          (*   (folded) method *)
        | Body tname stmt expr     (* (unfolded) method body *)
and  stmt
        = Skip                     (* empty      statement *)
        | Expr  expr               (* expression statement *)
        | Comp  stmt stmt          ("_;; _"                     [      66,65]65)
        | If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
        | Loop  expr stmt          ("While'(_') _"              [      80,79]70)
        | Throw expr
        | TryC  stmt
                tname ename stmt   ("Try _ Catch'(_ _') _"      [79,99,80,79]70)
        | Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
        | init  tname              (* class initialization *)

types term = "(expr+stmt, var, expr list) sum3"
translations
  "sig"   <= (type) "mname × ty list"
  "var"   <= (type) "Term.var"
  "expr"  <= (type) "Term.expr"
  "stmt"  <= (type) "Term.stmt"
  "term"  <= (type) "(expr+stmt, var, expr list) sum3"


syntax
  this :: expr
  LAcc :: "ename \<Rightarrow>         expr" ("!!")
  LAss :: "ename \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
translations
 "this"  == "Acc (LVar This)"
 "!!v"   == "Acc (LVar (EName v))"
 "v:==e" == "Ass (LVar (EName v)) e"
  
constdefs

  is_stmt :: "term \<Rightarrow> bool"
 "is_stmt t \<equiv> \<exists>c. t=In1r c"
  
end

theorems is_stmt_rews:

  is_stmt (In1l x) == False

  is_stmt (In2 x) == False

  is_stmt (In3 x) == False

  is_stmt (In1r x) == True

theorem is_stmtD:

  is_stmt t ==> EX c. t = In1r c