(*  Title:      isabelle/Bali/Basis.thy
    ID:         $Id: Basis.thy,v 1.7 1998/04/08 15:26:54 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Definitions extending HOL as logical basis of Bali
*)
Basis = Sum + WF Rel + Map + Integ + Inductive +

constdefs

  unique   :: "('a × 'b) list ⇒ bool"
 "unique t ≡ ∀(x,y)∈set t. ∀(x',y')∈set t. x = x' ⟶ y = y'"

end

(*  Title:      isabelle/Bali/Table.thy
  ID:         $Id: Table.thy,v 1.8 1998/04/08 15:27:05 oheimb Exp $
  Author:     David von Oheimb
  Copyright   1997 Technische Universitaet Muenchen
Abstract tables and their implementation as lists
design issues:
* definition of table: infinite map vs. list vs. finite set
list chosen, because:
+  a priori finite
+  lookup is more operational than for finite set
-  not very abstract, but function table converts it to abstract mapping
* coding of lookup result: Some/None vs. value/arbitrary
 Some/None chosen, because:
++ makes definedness check possible (applies also to finite set),
   which is important for the type system, hiding/overriding, etc.
   (though it may perhaps be possible at least for the operational semantics
    to treat programs as infinite, i.e. where classes, fields, methods etc.
    of any name are considered to be defined)
-  awkward case distinctions, alleviated by operator 'the'
*)
Table = Basis +
types ('a, 'b) table    (* table with key type 'a and contents type 'b *)
      = "'a ⇝ 'b"
    ('a, 'b) tables   (* non-unique table with key 'a and contents 'b *)
      = "'a ⇒ 'b set"

syntax

table of      :: "('a × 'b) list ⇒ ('a, 'b) table"   (* concrete table *)

translations

"table of" == "map of"

consts

Un tables     :: "('a, 'b) tables set ⇒ ('a, 'b) tables"
overrides     :: "('a, 'b) tables  ⇒ ('a, 'b) tables ⇒ ('a, 'b) tables"
                                                (infixl "⊕ ⊕" 100)
hidings entails:: "('a, 'b) tables ⇒ ('a, 'c) tables ⇒
                   ('b ⇒ 'c ⇒ bool) ⇒ bool"  ("  hidings   entails  " 20)
(* variant for unique table: *)
hiding entails :: "('a, 'b) table ⇒ ('a, 'c) table ⇒
                   ('b ⇒ 'c ⇒ bool) ⇒ bool"  ("  hiding   entails  "  20)

defs

Un tables def       "Un tables ts  ≡ λk. ⋃t∈ts. t k"
overrides def       "s ⊕ ⊕ t  ≡ λk. if t k = {} then s k else t k"
hidings entails def "t hidings s entails R ≡ ∀k. ∀x∈t k. ∀y∈s k. R x y"
hiding entails def  "t hiding  s entails R ≡
                      ∀k x. t k = Some x ⟶ (∀y. s k = Some y ⟶ R x y)"

end

(*  Title:      isabelle/Bali/Type.thy
ID:         $Id: Type.thy,v 1.7 1998/04/08 15:27:09 oheimb Exp $
Author:     David von Oheimb
Copyright   1997 Technische Universitaet Muenchen
Java types
simplifications:
* few primitive types yet
* arrays do not have special methods and fields like length
*)
Type = Table +
(* for names, cf. 6.5 *)
types tnam            (* type name, i.e. class or interface name *)
enam            (* expression name, i.e. variable or field name *)
mname           (* method name *)
arities tnam, enam, mname :: term
datatype xname  (* names of system exceptions *)
= Throwable
| NullPointer | OutOfMemory | ClassCast
| NegArrSize  | IndOutBound | ArrStore
datatype tname  (* type names for system classes and other type names *)
= Object
| SXcpt   xname
| TName   tnam
datatype ename  (* names for the This pointer and local variables *)
= This
| EName   enam

datatype prim ty        (* primitive type, cf. 4.2 *)
= Void          (* 'result type' of void methods *)
| Boolean
| Integer
(** parameter 'a circumvents mutual recursion with datatype ty **)
datatype 'a Rt          (* reference type, cf. 4.3 *)
= NullT         (* null type, cf. 4.1 *)
| IfaceT tname  (* interface type *)
| ClassT tname  (* class type *)
| ArrayT 'a     (* array type *)
datatype ty             (* any type, cf. 4.1 *)
= PrimT prim ty (* primitive type *)
| RefT (ty Rt)  (* reference type *)

types

         ref ty = ty Rt

translations

        "ref ty" <= (type) "ty Rt"

syntax

         NT     :: "          ty"
         Iface  :: "tname ⇒ ty"
         Class  :: "tname ⇒ ty"
         Array  :: "ref ty ⇒ ty"       (" [·]" [90] 90)

translations

        "NT"      == "RefT   NullT"
        "Iface I" == "RefT (IfaceT I)"
        "Class C" == "RefT (ClassT C)"
        "T[·]"    == "RefT (ArrayT T)"

end

(*  Title:      isabelle/Bali/Term.thy
    ID:         $Id: Term.thy,v 1.8 1998/04/08 15:27:06 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Java expressions and statements
design issues:
* all variables may alternatively be handled in a very uniform way, by
  representing arrays as special sort of class instances, and by
  representing the current invocation frame as an instance of a special pseudo
  class (one per method definition) and identifying a special location called
  StackTop (as opposed to Heap) pointing to it.
  Instead, we use a different approach for each kind of variable because:
  +  it is closer to the language and therefore easier to read
  +  there is no extra handling (e.g. invariants) for special constructs
     like StackTop needed
  -  there is more redundancy in the syntax and some semantic aspects
     of variable access and assignment
* for the transition semantics, the method call produces an intermediate method
  body construct that enables the restoration of the previous 'stack' contents.
simplifications:
* expression statement allowed for any expression
* no super yet
* no unary, binary, ..., operators
* The This pointer is modeled as a special non-assignable local variable
* access to field x in current class via This.x
* NewA creates just one-dimensional arrays;
  initialization of further subarrays may be simulated with nested NewAs
* no constructors, initializers and finalizers yet
* for simplicity, 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.
* no synchronized
* result expression instead of return statement (see Decl.thy)
* 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
* 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 = Type +
types loc     (* locations, i.e. abstract references on objects *)
arities loc :: term
datatype val  (** name not 'val' because of clash with ML token **)
        = Unit          (* dummy result value of void methods *)
        | Bool bool     (* Boolean value *)
        | Intg int      (* integer value *)
        | Null          (* null reference *)
        | Addr loc      (* addresses, i.e. locations of objects *)
types  val   =         val
translations "val" <= (type) "val "

consts

defpval       :: "prim ty ⇒ val"     (* default value for primitive types *)
default val   :: "     ty ⇒ val"     (* default value for all types *)
primrec defpval Type.prim ty
"defpval Void    = Unit"
"defpval Boolean = Bool False"
"defpval Integer = Intg ($#0)"
primrec default val Type.ty
"default val (PrimT pt) = defpval pt"
"default val (RefT  r ) = Null"

constdefs

the Bool   :: "val ⇒ bool"
"the Bool v ≡ εb. v = Bool b"
the Intg   :: "val ⇒ int"
"the Intg v ≡ εi. v = Intg i"
the Addr   :: "val ⇒ loc"
"the Addr v ≡ εa. v = Addr a"

datatype 'a e

= NewC  tname              (* class instance creation *)
| NewA  ty ('a e)          (* array creation *) ("New  [ ]"[90,10   ]90)
| Cast  ty ('a e)          (* type cast *)
| Lit   val                (* literal value, references not allowed *)
| LAcc  ename              (* local (incl. parameter) access *)
| LAss  ename        ('a e)(* local assignment *)(" := "[      99,80]70)
| FAcc ('a e) ref ty ename (* field access *) (" .{ } " [90,10,99   ]90)
| FAss ('a e) ref ty ename
                     ('a e)(* field ass. *)(" .{ } := " [80,10,99,80]70)
| AAcc ('a e)('a e)        (* array access *) (" [ ]"   [90,10      ]90)
| AAss ('a e)('a e)  ('a e)(* array ass. *)   (" [ ]:= "[80,10,   80]70)
| Call ('a e)mname ty('a e)(* method call*)(" .. { }'( ')" [80,10,99]80)
| Body  'a   ('a e) ((ename, val) table)  (* method body*)

datatype stmt

= Skip                     (* empty      statement *)
| Expr (stmt e)            (* expression statement *)
| Comp  stmt    stmt       (" ;;  "                     [      61,60]60)
| Cond (stmt e) stmt stmt  ("If'( ')   Else  "          [   80,79,79]70)
| Loop (stmt e) stmt       ("While'( ')  "              [      80,79]70)
| Throw(stmt e)
| TryC  stmt
         tname ename stmt  ("Try   Catch'(   ')  "      [79,80,80,79]70)
| Fin   stmt    stmt       ("  Finally  "               [      79,79]70)
types expr = stmt e

end

(*  Title:      isabelle/Bali/Decl.thy
    ID:         $Id: Decl.thy,v 1.7 1998/04/08 15:26:55 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Field, method, interface, and class declarations, whole Java programs
simplifications:
* no field  modifiers yet, i.e. every field  is public, non-static, non-final
* no method modifiers yet, i.e. every method is public, non-static, non-final
* no throws clause
* result statement replaced by result expression (evaluated at the end of the
  execution of the body; transformation is always possible (with goto, while)
* a void method is replaced by one that returns Unit of dummy type Void
* local variables are initialzed with default values
* each method has exactly one (explicit) parameter; this may be an object with
  as many fields as required if the method has more than one parameter
* no interface modifiers yet, i.e. every interface is public
* no interface fields yet
* no class modifiers yet, i.e. every class is public, non-final
* every class except Object has an explicit superclass
* Object does not have any standard methods
* no packages
* no main method yet
*)
Decl = Term +
types field
        = "ty"
        fdecl           (* field declaration, cf. 8.3 (, 9.3) *)
        = "ename × field"
types sig             (* signature of a method, cf. 8.4.2 *)
        = "mname × ty"  (* method name, parameter type *)
        mhead           (* method head (excluding signature) *)
        = "ename × ty"  (* parameter name, result type *)
        lvar            (* local variable *)
        = "ename × ty"
        mbody           (* method body *)
        = "lvar list × stmt × expr"
        (* local variables, block, result expression *)
        methd           (* method in a class *)
        = "mhead × mbody"
        mdecl           (* method declaration in a class *)
        = "sig × methd"

types iface           (* interface *)
        = "tname list × (sig × mhead) list"
        (* superinterface list, methods *)
        idecl           (* interface declaration, cf. 9.1 *)
        = "tname × iface"
types class           (* class *)
        = "tname option × tname list × fdecl list × mdecl list"
        (* superclass, implemented interfaces, fields, methods*)
        cdecl           (* class declaration, cf. 8.1 *)
        = "tname × class"

consts

  ObjectC ::          "cdecl"   (* declaration  of root      class   *)
  SXcptC  :: "xname ⇒ cdecl"   (* declarations of throwable classes *)

defs

 ObjectC def    "ObjectC ≡ (Object  , (None                  , [], [], []))"
 SXcptC def     "SXcptC xn≡ (SXcpt xn, (Some (if xn = Throwable then Object else
                                               SXcpt Throwable), [], [], []))"
types prog = "idecl list × cdecl list"

syntax

  iface         :: "prog ⇒ (tname, iface) table"
  class         :: "prog ⇒ (tname, class) table"

translations

                "iface G"     == "table of (fst G)"
                "class G"     == "table of (snd G)"

consts

  is iface      :: "prog ⇒ tname ⇒ bool"
  is class      :: "prog ⇒ tname ⇒ bool"
  is type       :: "prog ⇒  ty ⇒ bool"
  isrtype       :: "prog ⇒ ref ty ⇒ bool"

defs

  is iface def  "is iface G I ≡ iface G I ≠ None"
  is class def  "is class G C ≡ class G C ≠ None"
primrec is type    ty
       "is type G (PrimT pt) = True"
       "is type G (RefT  rt) = isrtype G rt"
primrec isrtype    Rt (** ref ty **)
       "isrtype G (NullT    ) = True"
       "isrtype G (IfaceT tn) = is iface G tn"
       "isrtype G (ClassT tn) = is class G tn"
       "isrtype G (ArrayT T ) = is type  G T"

(* general operators for recursion over the interace and class hiearchies *)
iface rec     :: "  tname × prog ×  (tname ⇒ iface ⇒ 'a set ⇒ 'a) ⇒ 'a"
class rec     :: "  tname × prog × 'a × (tname ⇒ class ⇒ 'a  ⇒ 'a) ⇒ 'a"
(* auxiliary relations for recursive definitions below *)
iface wfrel   :: "((tname × prog ×  (tname ⇒ iface ⇒ 'a set ⇒ 'a)) ×
                   (tname × prog ×  (tname ⇒ iface ⇒ 'a set ⇒ 'a))) set"
class wfrel   :: "((tname × prog × 'a × (tname ⇒ class ⇒ 'a  ⇒ 'a)) ×
                   (tname × prog × 'a × (tname ⇒ class ⇒ 'a  ⇒ 'a))) set"
recdef iface rec "iface wfrel" congs "[image cong]"
"iface rec (I,G,  f) = (if (∀i J. iface G I = Some i ∧ J ∈ set (fst i) ⟶
                                 ((J,G,  f), (I,G,  f)) ∈ iface wfrel)
                      then (case iface G I of None ⇒ arbitrary | Some i ⇒
                            f I i ((λJ. iface rec (J,G,  f))``set (fst i)))
                      else arbitrary)"
recdef class rec "class wfrel"
"class rec (C,G,t,f) = (if (∀c D. class G C = Some c ∧ Some D = (fst c) ⟶
                                 ((D,G,t,f), (C,G,t,f)) ∈ class wfrel)
                      then (case class G C of None ⇒ arbitrary | Some c ⇒
                            f C c (case (fst c) of None ⇒ t | Some D ⇒
                                        class rec (D,G,t,f)))
                      else arbitrary)"

consts

imethds       :: "prog ⇒ tname ⇒ ( sig   , ref ty × mhead) tables"
cmethd        :: "prog ⇒ tname ⇒ ( sig   , ref ty × methd) table"
cfield        :: "prog ⇒ tname ⇒ ( ename , ref ty × field) table"
fields        :: "prog ⇒ tname ⇒ ((ename × ref ty) × field) list"

defs

(* methods of an interface, with overriding and inheritance, cf. 9.2 *)
imeths def "imethds G I ≡ iface rec (I,G,      (λI (is,ms)       ts.
     (Un tables ts) ⊕ ⊕ (o2s ∘ table of (map (λ(s,mh). (s,IfaceT I,mh)) ms))))"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
cmethd def "cmethd  G C ≡ class rec (C,G,empty,(λC (sc,si,fs,ms) ts.
                         ts ⊕ table of (map (λ(s,m ). (s,(ClassT C,m))) ms)))"
(* list of fields implemented by a class, including inherited and hidden ones *)
 fields def "fields G C ≡ class rec (C,G,[]   ,(λC (sc,si,fs,ms) ts.
                                  map (λ(fn,ft).((fn,ClassT C),ft)) fs @ ts))"
(* fields of a class, with inheritance and hiding, cf. 8.3 *)
cfield def  "cfield G C ≡ table of((map (λ((n,d),t).(n,(d,t)))) (fields G C))"

end

(*  Title:      isabelle/Bali/TypeRel.thy
  ID:         $Id: TypeRel.thy,v 1.9 1998/04/08 15:27:11 oheimb Exp $
  Author:     David von Oheimb
  Copyright   1997 Technische Universitaet Muenchen
The relations between Java types
*)
TypeRel = Decl +

consts

subint1,                                         (* direct subinterface   *)
subint        :: "prog ⇒ (tname × tname) set"   (*        subinterface   *)
subcls1,                                         (* direct subclass       *)
subcls        :: "prog ⇒ (tname × tname) set"   (*        subclass       *)
implmt1,                                         (* direct implementation *)
implmt        :: "prog ⇒ (tname × tname) set"   (*        implementation *)
widen,                                           (*        widening       *)
cast          :: "prog ⇒ (ty × ty   ) set"   (*        casting        *)
syntax (symbols)
subint1       :: "prog ⇒ [tname, tname] ⇒ bool" (" ⊢ ≺I1 "[71,71,71] 70)
subint        :: "prog ⇒ [tname, tname] ⇒ bool" (" ⊢ ≺I  "[71,71,71] 70)
subcls1       :: "prog ⇒ [tname, tname] ⇒ bool" (" ⊢ ≺C1 "[71,71,71] 70)
subcls        :: "prog ⇒ [tname, tname] ⇒ bool" (" ⊢ ≺C  "[71,71,71] 70)
implmt1       :: "prog ⇒ [tname, tname] ⇒ bool" (" ⊢ ⇝1 " [71,71,71] 70)
implmt        :: "prog ⇒ [tname, tname] ⇒ bool" (" ⊢ ⇝ "  [71,71,71] 70)
widen         :: "prog ⇒ [ty   , ty   ] ⇒ bool" (" ⊢ ⪯ "  [71,71,71] 70)
cast          :: "prog ⇒ [ty   , ty   ] ⇒ bool" (" ⊢ ⪯?  "[71,71,71] 70)

translations

      "G ⊢ I ≺I1 J" == "(I,J) ∈ subint1 G"
      "G ⊢ I ≺I  J" == "(I,J) ∈ subint  G"
      "G ⊢ C ≺C1 D" == "(C,D) ∈ subcls1 G"
      "G ⊢ C ≺C  D" == "(C,D) ∈ subcls  G"
      "G ⊢ C ⇝1  I" == "(C,I) ∈ implmt1 G"
      "G ⊢ C ⇝ I" == "(C,I) ∈ implmt  G"
      "G ⊢ S ⪯ T" == "(S,T) ∈ widen   G"
      "G ⊢ S ⪯?  T" == "(S,T) ∈ cast    G"

defs

(* direct subinterface, cf. 9.1.3 *)
subint1 def   "subint1 G ≡ {(I,J). is iface G I ∧ is iface G J ∧
                                    J∈set      (fst (the (iface G I)))}"
(* direct subclass, cf. 8.1.3 *)
subcls1 def   "subcls1 G ≡ {(C,D). is class G C ∧ is class G D ∧
                                    Some D =    fst (the (class G C))}"
(* direct implementation, cf. 8.1.3 *)
implmt1 def   "implmt1 G ≡ {(C,I). is class G C ∧ is iface G I ∧
                                    I∈set (fst (snd (the (class G C))))}"

inductive "subint G" intrs (* subinterface relation, cf. 9.1.3 *)
direct         "G ⊢ I≺I1K  ⟹ G ⊢ I≺I K"
trans         "[[ G ⊢ I≺I J; G ⊢ J≺I K ]] ⟹ G ⊢ I≺I K"
inductive "subcls G" intrs (* subclass relation, cf. 8.1.3 *)
direct         "G ⊢ C≺C1E  ⟹ G ⊢ C≺C E"
trans         "[[ G ⊢ C≺C D; G ⊢ D≺C E ]] ⟹ G ⊢ C≺C E"
inductive "implmt G" intrs              (* cf. 8.1.4 *)
direct         "G ⊢ C⇝1J  ⟹ G ⊢ C⇝J"
subint        "[[ G ⊢ C⇝1I; G ⊢ I≺I J ]] ⟹ G ⊢ C⇝J"
subcls1       "[[ G ⊢ C≺C1D; G ⊢ D⇝J ]] ⟹ G ⊢ C⇝J"

inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
                          i.e. sort of syntactic subtyping *)
refl   "is type G T  ⟹ G ⊢  T⪯T"   (* identity conv., cf. 5.1.1 *)
subint "G ⊢ I≺I J  ⟹ G ⊢ Iface I⪯Iface J"(*wid. ref.conv,cf. 5.1.4 *)
int obj"is iface G I  ⟹
        is class G Object  ⟹ G ⊢ Iface I⪯Class Object"
subcls "G ⊢ C≺C D  ⟹ G ⊢ Class C⪯Class D"
implmt "G ⊢ C⇝I  ⟹ G ⊢ Class C⪯Iface I"
null   "is type G  (RefT R) ⟹ G ⊢  NT⪯RefT R"
arr obj"is type G T  ⟹
        is class G Object  ⟹ G ⊢  T[·]⪯Class Object"
array  "G ⊢ RefT S⪯RefT T  ⟹ G ⊢ RefT  S[·]⪯RefT T[·]"
inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
widen  "G ⊢ S⪯T  ⟹ G ⊢  S⪯? T"
subcls "G ⊢ C≺C D  ⟹ G ⊢  Class D⪯? Class C"
implmt "is class G C  ⟹
        is iface G I  ⟹ G ⊢  Class C⪯? Iface I"
obj arr"is class G Object  ⟹
        is type G T  ⟹ G ⊢ Class Object⪯? T[·]"
int cls"is iface G I  ⟹
        is class G C  ⟹ G ⊢  Iface I⪯? Class C"
subint "is iface G I  ⟹
        is iface G J  ⟹
        imethds G I hidings imethds G J
                    entails (λ(md,(pn,rT)) (md',(pn',rT')). G ⊢ rT⪯rT') ⟹
        ¬G ⊢ I≺I J  ⟹ G ⊢  Iface I⪯? Iface J"
array  "G ⊢ RefT S⪯? RefT T ⟹ G ⊢ RefT S[·]⪯? RefT T[·]"

end

(*  Title:      isabelle/Bali/WellType.thy
    ID:         $Id: WellType.thy,v 1.7 1998/04/08 15:27:14 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Well-typedness of Java programs
the formulation of well-typedness of method calls given below (as well as
the Java Specification 1.0) is a little too restrictive: Is does not allow
methods of class Object to be called upon references of interface type.
simplifications:
* the type rules include all static checks on expressions and statements, e.g.
  definedness of names (of parameters, locals, fields, methods)
design issues:
* the typing rules take an extra argument that is capable of determining
  the dynamic type of objects. Therefore, they can be used for both
  checking static types and determining runtime types in transition semantics.
*)
WellType = TypeRel +

types lenv

        = "(ename, ty) table"   (* local variables, including This *)
        env
        = "prog × lenv"         (* program, locals *)
        dyn ty
        = "loc ⇒ ty option"

syntax

  prg   :: "env ⇒ prog"
  lcl   :: "env ⇒ lenv"

translations

  "prg" => "fst"
  "lcl" => "snd"

consts

  more spec     :: "prog ⇒ (ref ty × mhead) × ty ⇒ (ref ty × mhead) × ty ⇒ bool"
  mheads        :: "prog ⇒ ref ty ⇒ sig  ⇒ (ref ty × mhead)         set"
  appl methds   :: "prog ⇒ ref ty ⇒ sig  ⇒((ref ty × mhead) × ty)   set"
  max spec      :: "prog ⇒ ref ty ⇒ sig  ⇒((ref ty × mhead) × ty)   set"

primrec mheads Rt (** ref ty **)
 "mheads G   NullT    = (λsig. {})"
 "mheads G (IfaceT I) = imethds G I"
 "mheads G (ClassT C) = o2s ∘ option map (λ(md,(mh,mb)).(md,mh)) ∘ cmethd G C"
 "mheads G (ArrayT T) = (λsig. {})"

defs

  more spec def   "more spec G ≡ λ((md,mh),pT). λ((md',mh'),pT').
                                 G ⊢ RefT md⪯RefT md'∧ G ⊢ pT⪯pT'"
  (* applicable methods, cf. 15.11.2.1 *)
  appl methds def "appl methds G T ≡ λ(mn, pT). {(mh,pT') |mh pT'.
                    mh ∈ mheads G T (mn, pT') ∧ G ⊢ pT⪯pT'}"
  (* maximally specific methods, cf. 15.11.2.2 *)
   max spec def   "max spec G T sig ≡ {m. m ∈appl methds G T sig ∧
                                         (∀m'∈appl methds G T sig.
                                                   more spec G m' m ⟶ m' = m)}"

consts

  typeof :: "dyn ty ⇒ val ⇒ ty option"
primrec typeof val  (** val **)
        "typeof dt  Unit    = Some (PrimT Void)"
        "typeof dt (Bool b) = Some (PrimT Boolean)"
        "typeof dt (Intg i) = Some (PrimT Integer)"
        "typeof dt  Null    = Some NT"
        "typeof dt (Addr a) = dt a"

consts

  ty exprs      :: " env ⇒ dyn ty ⇒ (expr × ty) set"
  wt stmts      :: "(env × dyn ty × stmt     ) set"
(*wt stmts      :: " env ⇒ dyn ty ⇒ stmt       set" not feasible because of
                                                       changing env in Try stmt *)

syntax

  ty expr :: "env ⇒ dyn ty ⇒ [expr,ty] ⇒ bool" (" , ⊧ :: "  [51,51,51,51] 50)
  wt stmt :: "env ⇒ dyn ty ⇒ stmt  ⇒ bool" (" , ⊧ ::◇" [51,51,51   ] 50)

translations

        "E,dt⊧ex::T"  == "(ex,T) ∈ ty exprs E dt"
        "E,dt⊧s ::◇" == "(E,dt,s) ∈ wt stmts"

syntax

  ty expr       :: "env ⇒ [expr, ty] ⇒ bool"    (" ⊢ :: "  [51,51,51] 50)
  wt stmt       :: "env ⇒ stmt  ⇒ bool"    (" ⊢ ::◇" [51,51   ] 50)
constdefs empty dt :: dyn ty "empty dt ≡ λa. None" (* for static typing *)

translations

        "E ⊢ ex::T"  == "E,empty dt⊧ex::T"
        "E ⊢ s ::◇" == "E,empty dt⊧s ::◇"

inductive "ty exprs E dt" intrs (* well-typed expressions *)
(* cf. 15.8 *)
NewC  "[[ is class (prg E) C ]] ⟹
                                               E,dt⊧NewC C::Class C"
(* cf. 15.9 *)
NewA  "[[ is type (prg E) T;
        E,dt⊧i::PrimT Integer ]] ⟹
                                               E,dt⊧New T[i]::T[·]"
(* cf. 15.15 *)
Cast  "[[ E,dt⊧e::T;
        prg E ⊢ T⪯? T' ]] ⟹
                                               E,dt⊧Cast T' e::T'"
(* cf. 15.7.1 *)
Lit   "[[ typeof dt x = Some T ]] ⟹
                                               E,dt⊧Lit x::T"
(* cf. 15.13.1 *)
LAcc  "[[ lcl E vn = Some T; is type (prg E) T ]] ⟹
                                               E,dt⊧LAcc vn::T"
(* cf. 15.25, 15.25.1 *)
LAss  "[[ E,dt⊧LAcc vn::T; vn ≠ This;
        E,dt⊧v  ::T';

        prg E ⊢ T'⪯T ]] ⟹
                                               E,dt⊧vn:=v::T'"

(* cf. 15.10.1 *)
FAcc  "[[ E,dt⊧a::Class C;
        cfield (prg E) C fn = Some (fd,fT) ]] ⟹
                                               E,dt⊧a.{fd}fn::fT"
(* cf. 15.25, 15.25.1 *)
FAss  "[[ E,dt⊧a.{fd}fn::T;
        E,dt⊧v  ::T';

        prg E ⊢ T'⪯T ]] ⟹

                                               E,dt⊧a.{fd}fn:=v::T'"
(* cf. 15.12 *)
AAcc  "[[ E,dt⊧a::T[·];
        E,dt⊧i::PrimT Integer ]] ⟹

                                               E,dt⊧a[i]::T"

(* cf. 15.25, 15.25.1 *)
AAss  "[[ E,dt⊧a[i]::T;
        E,dt⊧v ::T';

        prg E ⊢ T'⪯T ]] ⟹
                                               E,dt⊧a[i]:=v::T'"

(* cf. 15.11.1, 15.11.2, 15.11.3 *)
Call  "[[ E,dt⊧a::RefT T;
        E,dt⊧p::pT;
        max spec (prg E) T (mn, pT) = {((md,(pn,rT)),pT')}]] ⟹
                                               E,dt⊧a..mn{pT'}(p)::rT"

inductive wt stmts intrs (* well-typed statements *)
Skip                                  "E,dt⊧Skip::◇"
Expr  "[[ E,dt⊧e::T ]] ⟹
                                       E,dt⊧Expr e::◇"
Comp  "[[ E,dt⊧c1::◇;

E,dt⊧c2::◇ ]] ⟹

                                       E,dt⊧c1;; c2::◇"

(* cf. 14.8 *)
Cond  "[[ E,dt⊧e::PrimT Boolean;
        E,dt⊧c1::◇;

E,dt⊧c2::◇ ]] ⟹

                                       E,dt⊧If(e) c1 Else c2::◇"
(* cf. 14.10 *)
Loop  "[[ E,dt⊧e::PrimT Boolean;

E,dt⊧c::◇ ]] ⟹

                                       E,dt⊧While(e) c::◇"
(* cf. 14.16 *)
Throw "[[ E,dt⊧e::Class tn;
        prg E ⊢ Class tn⪯Class (SXcpt Throwable) ]] ⟹
                                       E,dt⊧Throw e::◇"
(* cf. 14.18 *)
Try   "[[ E,dt⊧c1::◇; prg E ⊢ Class tn⪯Class (SXcpt Throwable);
        lcl E vn = None; (prg E,lcl E[vn↦Class tn]),dt⊧c2::◇ ]] ⟹
                                       E,dt⊧Try c1 Catch(tn vn) c2::◇"
(* cf. 14.18 *)
Fin   "[[ E,dt⊧c1::◇; E,dt⊧c2::◇ ]] ⟹
                                       E,dt⊧c1 Finally c2::◇"

end

(*  Title:      isabelle/Bali/WellForm.thy
  ID:         $Id: WellForm.thy,v 1.10 1998/04/08 15:27:12 oheimb Exp $
  Author:     David von Oheimb
  Copyright   1997 Technische Universitaet Muenchen
Well-formedness of Java programs
for static checks on expressions and statements, see WellType.thy
improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
* a method implementing or overwriting another method may have a result type
that widens to the result type of the other method (instead of identical type)
* if an interface inherites more than one method with the same signature, the
methods need not have identical return types
simplifications:
* for uniformity, Object is assumed to be declared like any other class
*)
WellForm = WellType +

consts

wf fdecl      :: "prog ⇒  fdecl ⇒ bool"
wf mhead      :: "prog ⇒ sig ⇒ mhead ⇒ bool"
wf mdecl      :: "prog ⇒ tname ⇒ mdecl ⇒ bool"
wf idecl      :: "prog ⇒  idecl ⇒ bool"
wf cdecl      :: "prog ⇒  cdecl ⇒ bool"
wf prog       :: "prog ⇒  bool"

defs

(* well-formed field declaration (common part for classes and interfaces),
   cf. 8.3 and (9.3) *)
wf fdecl def  "wf fdecl G ≡ λ(fn,ft). is type G ft"
(*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
(* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
wf mhead def  "wf mhead G ≡ λ(mn,pT) (pn,rT). is type G pT ∧
                                               is type G rT ∧ pn ≠ This"
wf mdecl def  "wf mdecl G C ≡ λ((mn,pT),(pn,rT),lvars,blk,res).
              let ltab = table of lvars; E=(G,ltab[This↦Class C][pn↦pT])
              in wf mhead G      (mn,pT) (pn,rT) ∧
                 unique lvars ∧ ltab This = None ∧ ltab pn = None ∧
                 (∀(vn,T)∈set lvars. is type G T) ∧
                 E ⊢ blk::◇ ∧ (∃T. E ⊢ res::T ∧ G ⊢ T⪯rT)"
(* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3 *)
wf idecl def  "wf idecl G ≡ λ(I,(is,ms)).
              ¬is class G I ∧
              (∀J  ∈set is. is iface G J) ∧
              (∀J  ∈set is. ¬ G ⊢ J≺I I)  ∧
              (∀(s,m)∈set ms. wf mhead G s m) ∧ unique ms ∧
              (o2s ∘ table of ms hidings
               Un tables ((λJ. (imethds G J))``set is) entails
               (λ(pn,rT) (md,(pn',rT')). G ⊢ rT⪯rT'))"

(* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
wf cdecl def  "wf cdecl G ≡ λ(C,(sc,si,fs,ms)).
¬is iface G C ∧
(∀I∈set si. is iface G I ∧
     (∀s. ∀(md',(pn',rT')) ∈ imethds G I s.
     (∃md pn rT b. cmethd G C s = Some (md,((pn,rT),b)) ∧
                   G ⊢ rT⪯rT'))) ∧
(∀f∈set fs. wf fdecl G   f) ∧ unique fs ∧
(∀m∈set ms. wf mdecl G C m) ∧ unique ms ∧
(case sc of None ⇒ C = Object | Some D ⇒
           is class G D ∧ ¬ G ⊢ D≺C C ∧
           (table of ms hiding cmethd G D
         entails (λ((pn,rT),b) (md,((pn',rT'),b')). G ⊢ rT⪯rT')))"
(* well-formed program, cf. 8.1, 9.1 *)
wf prog def   "wf prog G ≡ let is = set (fst G); cs = set (snd G) in
        ObjectC ∈ cs ∧ (∀xn. SXcptC xn ∈ cs) ∧
(∀i∈is. wf idecl G i) ∧ unique (fst G) ∧
(∀c∈cs. wf cdecl G c) ∧ unique (snd G)"

defs

(* well-founded relations for termination proofs for iface rec and class rec *)
iface wfrel def "iface wfrel ≡ {((I,G, f),(I',G', f')). (G, f) = (G', f') ∧
                  wf ((subint1 G)^-1) ∧ (I,I')∈(subint1 G)^-1}"
class wfrel def "class wfrel ≡ {((C,G,tf),(C',G',tf')). (G,tf) = (G',tf') ∧
                  wf ((subcls1 G)^-1) ∧ (C,C')∈(subcls1 G)^-1}"

end

(*  Title:      isabelle/Bali/State.thy
    ID:         $Id: State.thy,v 1.8 1998/04/08 15:27:03 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
State for evaluation of Java expressions and statements
design issues:
* new Addr fails iff there is no free heap address. At the latest when there is
  only one free heap address left, it returns an OutOfMemory exception.
  In this way it is guaranteed that when an OutOfMemory exception is thrown for
  the first time, there is a free location on the heap to allocate it.
* unfortunately new Addr is not directly executable because of Hilbert operator.
simplifications:
* lconf is designed to allow for (arbitrary) inaccessible values
* the stack of invocation frames containing local variables and return addresses
  for method calls is not explicitly modeled, nor finiteness constrains on it.
* garbage collection not considered
*)
State = WellForm +
types fields  (** clash with TypeRel.fields **)
        = "(ename × ref ty, val) table" (* field name, defining class, value *)
        components
        = "(int           , val) table" (* array elements *)
datatype obj    (* object *)
        = Obj tname fields      (* class instance with class name and fields *)
        | Arr ty    components  (* array with component type and components *)

consts

  the Obj       :: "obj option ⇒ tname × fields "
  the Arr       :: "obj option ⇒ ty × components"
  obj ty        :: "obj ⇒ ty"

defs

 the Obj def    "the Obj obj ≡ ε(C,fs). obj = Some (Obj C fs)"
 the Arr def    "the Arr obj ≡ ε(T,cs). obj = Some (Arr T cs)"
primrec obj ty obj
 "obj ty (Obj C fs) = Class C"
 "obj ty (Arr T cs) = T[·]"

datatype xcpt   (* exception *)
        = XcptLoc loc   (* location of allocated execption object *)
        | SysXcpt xname (* intermediate system exception, see Eval.thy *)

the XcptLoc   :: "xcpt ⇒ loc"
the SysXcpt   :: "xcpt ⇒ xname"

defs

the XcptLoc def       "the XcptLoc xc ≡ εa. xc = XcptLoc a"
the SysXcpt def       "the SysXcpt xc ≡ εx. xc = SysXcpt x"
types aheap           (* heap *)
      = "(loc, obj) table"
      locals          (* local variables *)
      = "(ename, val) table"
      st              (* pure state, i.e. contents of all variables *)
      = "aheap × locals"
      (* heap, locals including This *)
      state           (* state including exception information *)
       = "xcpt option × st"

syntax

heap          :: "st ⇒ aheap"
locals        :: "st ⇒ locals"
Norm          :: "st ⇒ state"

translations

"heap"        => "fst"
"locals"      => "snd"
"Norm s"      == "(None,s)"

consts

xcpt ty       :: "st ⇒ xcpt ⇒ ty"
primrec xcpt ty xcpt
     "xcpt ty st (XcptLoc a ) = obj ty (the (heap st a))"
     "xcpt ty st (SysXcpt xn) = Class (SXcpt xn)"

constdefs

new Addr      :: "aheap ⇒ (loc × xcpt option) option"
"new Addr h  ≡ εy.        y = None ∧ (∀a. h a ≠ None) ∨
                     (∃a x. y = Some (a,x) ∧ h a = None ∧
                           (x = None ∨ x = Some (SysXcpt OutOfMemory)))"
init vars     :: "('a × ty) list ⇒ ('a, val) table"
"init vars  ≡ table of ∘ map (λ(n,T). (n,default val T))"
init Obj      :: "prog ⇒ tname ⇒ obj"
"init Obj G C ≡ Obj C (init vars (fields G C))"
init Arr      :: "ty ⇒ int ⇒ obj"
"init Arr T i ≡Arr T (λj. if $#0≤j ∧ j<i then Some (default val T) else None)"

raise if      :: "bool ⇒ xname ⇒ xcpt option ⇒ xcpt option"
"raise if c xn xo ≡ if c ∧ (xo = None) then Some (SysXcpt xn) else xo"
  lupd        :: "ename ⇒ val ⇒ st ⇒ st"        ("lupd[ ↦ ]  " [900,0,99] 900)
"  lupd vn v ≡ λ(h,l). (h,l[vn↦v])"
  hupd        :: "loc ⇒ obj ⇒ st ⇒ st"          ("hupd[ ↦ ]  " [900,0,99] 900)
"  hupd a obj ≡ λ(h,l). (h[a↦obj],l)"
c hupd        :: "loc ⇒ obj ⇒ state ⇒ state" ("c' hupd[ ↦ ]  " [900,0,99] 900)
"c hupd a obj ≡ λ(x,s). (x, if x = None then hupd[a↦obj] s else s)"

syntax

np            :: "val ⇒ xcpt option ⇒ xcpt option"

translations

"np v" == "raise if (v = Null) NullPointer"

constdefs

hext  :: "aheap ⇒ aheap ⇒ bool"               (     " ≤| "     [51,51]       50)
         "h≤|h' ≡ ∀a obj.  h  a = Some obj ⟶
                     (∃obj'. h' a = Some obj' ∧ obj ty obj' = obj ty obj)"
fits  :: "prog ⇒ aheap ⇒ val ⇒ ty ⇒ bool"   (" , ⊢ fits  "  [51,51,51,51] 50)
"G,h ⊢ v fits T ≡ ((∃pt. T=PrimT pt) ∨ v=Null ∨ G ⊢ obj ty (the(h(the Addr v)))⪯T)"
conf  :: "prog ⇒ aheap ⇒ val ⇒ ty ⇒ bool"   (" , ⊢ ::⪯ "     [51,51,51,51] 50)
         "G,h ⊢ v::⪯T ≡ ∃T'. typeof (option map obj ty ∘ h) v = Some T' ∧ G ⊢ T'⪯T"
lconf :: "prog ⇒ aheap ⇒ ('a, val) table ⇒ ('a, ty) table ⇒ bool"
                                                (" , ⊢ [::⪯] "   [51,51,51,51] 50)
         "G,h ⊢ vs[::⪯]Ts≡ ∀n T. Ts n = Some T ⟶ (∃v. vs n = Some v ∧ G,h ⊢ v::⪯T)"

consts

oconf :: "prog ⇒ aheap ⇒ obj ⇒ bool"         (" , ⊢ ::⪯ ◇"     [51,51,51]    50)
primrec oconf obj
"G,h ⊢ Obj C fs::⪯ ◇ = (G,h ⊢ fs[::⪯]table of   (fields G C))"
"G,h ⊢ Arr T cs::⪯ ◇ = (G,h ⊢ cs[::⪯]option map (λi. T) ∘ cs)"

constdefs

conforms :: "state ⇒ env ⇒ bool"              (     " ::⪯ "      [51,51]       50)
            "xs::⪯E ≡ let G = prg E; s = snd xs; h = heap s; l = locals s in
         (∀a obj. h a = Some obj  ⟶ G,h ⊢ obj  ::⪯ ◇  ) ∧
                                            G,h ⊢  l[::⪯](lcl E) ∧
         (∀a. fst xs = Some (XcptLoc a) ⟶ G,h ⊢ Addr a ::⪯ Class(SXcpt Throwable))"

end

(*  Title:      isabelle/Bali/Eval.thy
  ID:         $Id: Eval.thy,v 1.9 1998/04/08 15:26:57 oheimb Exp $
  Author:     David von Oheimb
  Copyright   1997 Technische Universitaet Muenchen
Operational evaluation (big-step) semantics of the
execution of Java expressions and statements
improvements over Java Specification 1.0:
* dynamic method lookup does not need to check the return type (cf. 15.11.4.4)
* throw raises a NullPointer exception if a null reference is given, and each
throw of a system exception yield a fresh exception object (was not specified)
* if there is not enough memory even to allocate an OutOfMemory exception,
evaluation/execution fails, i.e. simply stops (was not specified)
design issues:
* evaluation vs. (one-step) transition semantics
evaluation semantics chosen, because:
++ less verbose and therefore easier to read (and to handle in proofs)
+  more abstract
+  intermediate values (appearing in recursive rules) need not be stored
   explicitly, e.g. no call body construct necessary as opposed to trans. sem.
+  convenient rule induction for subject reduction theorem
-  no interleaving (for parallelism) describable
-  stating a property of infinite executions requires the meta-level argument
   that this property holds for any finite prefixes of it (e.g. stopped using
   a counter that is decremented to zero and then throwing an exception)
* the value entry in rules is redundant in case of exceptions, but its full
inclusion helps to make the rule structure independent of exception occurence.
* the rule format is such that the start state may contain an exception.
++ faciliates exception handling
+  symmetry
* the rules are defined carefully in order to be applicable even in not
type-correct situations (yielding undefined values),
e.g. the Adr (Val (Bool b)) = arbitrary.
++ fewer rules
-  less readable because of auxiliary functions like the Adr
Alternative: "defensive" evaluation throwing some InternalError exception
             in case of (impossible, for correct programs) type mismatches
* the allocation of objects that represent system exceptions is deferred until
the end of the (if any) enclosing try block; this helps to avoid (conditional)
side effects on the heap and problems with out-of-memory conditions
* there is exacly one rule (except for Try Catch) per syntactic construct
+ no redundancy in case distinctions
rule split for Try Catch because of conditional execution of its catch clause,
which would require recursion in a conditional formula (not permitted by the
current implementation of the inductive package) or the alternative execution
of a Skip statement (requires several occurences of the case distinction)
* if a system exception is raised while evaluating an expression, the allocation
of a corresponding exceptions is deferred until execution of some statement
after it, but before any catch clause. This is transparent to the program.
-  a kind of non-determinism
-  an extra, even not syntax-driven, rule (SXcpt)
+  extra rule avoids redundany in the two Try Catch rules
++ avoids copies of allocation code and awkward case distinctions (whether
   there is enough memory to allocate the exception) in evaluation rules
*)

Eval = State +

consts

eval  :: "prog ⇒ (state × (expr × val) × state) set"
exec  :: "prog ⇒ (state × stmt  × state) set"
syntax (symbols)
eval :: "[prog,state,expr,val,state] ⇒ bool "(" ⊢ − ≻ → "[51,82,82,82,82]81)
exec :: "[prog,state,stmt,    state] ⇒ bool "(" ⊢ − → "   [51,82,82,   82]81)

translations

"G ⊢ s −e0≻v→ s'" == "(s, (e0,v), s') ∈ eval G"
"G ⊢ s −s0 → s'" == "(s,  s0   , s') ∈ exec G"
inductive "eval G" "exec G" intrs
(* evaluation of expressions *)
(* cf. 15.5 *)
XcptE             "G ⊢ (Some xc,s) −e≻arbitrary→ (Some xc,s)"
(* cf. 15.8.1 *)
NewC  "[[ new Addr (heap s) = Some (a,x) ]] ⟹
                      G ⊢ Norm s −NewC C≻Addr a→ c hupd[a↦init Obj G C](x,s)"
(* cf. 15.9.1 *)
NewA  "[[ G ⊢ Norm s0 −e≻i'→ (x1,s1); i = the Intg i';
        new Addr (heap s1) = Some (a,x);
        x1' = raise if (i<$#0) NegArrSize (if x1 = None then x else x1) ]] ⟹
                   G ⊢ Norm s0 −New T[e]≻Addr a→ c hupd[a↦init Arr T i](x1',s1)"
(* cf. 15.15 *)
Cast  "[[ G ⊢ Norm s0 −e≻v→ (x1,s1);
        x2 = raise if (¬G,heap s1 ⊢ v fits T) ClassCast x1 ]] ⟹
                              G ⊢ Norm s0 −Cast T e≻v→ (x2,s1)"
(* cf. 15.7.1 *)
Lit                              "G ⊢ Norm s −Lit v≻v→ Norm s"
(* cf. 15.13.1, 15.2, 15.7.2 *)
LAcc           "G ⊢ Norm s −LAcc vn≻the (locals s vn)→ Norm s"
(* cf. 15.25.1 *)
LAss  "[[ G ⊢ Norm s0 −e≻v→ (x,s1);
        s1' = (if x = None then lupd[vn↦v]s1 else s1) ]] ⟹
                               G ⊢ Norm s0 −(vn:=e)≻v→ (x,s1')"

(* cf. 15.10.1, 15.2 *)
FAcc  "[[ G ⊢ Norm s0 −e≻a'→ (x1,s1);
        v = the (snd (the Obj (heap s1 (the Addr a'))) (fn,T)) ]] ⟹
                               G ⊢ Norm s0 −e.{T}fn≻v→ (np a' x1,s1)"

(* cf. 15.25.1 *)
FAss  "[[ G ⊢  Norm s0 −e1≻a'→ (x1,s1); a = the Addr a';
        G ⊢ (np a' x1,s1) −e2≻v → (x2,s2);
        (c,fs) = the Obj (heap s2 a); obj = Obj c (fs[(fn,T)↦v]) ]] ⟹
                        G ⊢ Norm s0 −(e1.{T}fn:=e2)≻v→ c hupd[a↦obj](x2,s2)"
(* cf. 15.12.1 *)
AAcc  "[[ G ⊢ Norm s0 −e1≻a'→  s1 ;
        G ⊢  s1 −e2≻i'→ (x2,s2);
        vo = snd (the Arr (heap s2 (the Addr a'))) (the Intg i');
        x3 = raise if (vo = None) IndOutBound (np a' x2) ]] ⟹
                           G ⊢ Norm s0 −e1[e2]≻the vo→ (x3,s2)"
(* cf. 15.25.1 *)
AAss  "[[ G ⊢ Norm s0 −e1≻a'→  s1 ; a = the Addr a';
        G ⊢  s1 −e2≻i'→  s2 ; i = the Intg i';
        G ⊢  s2 −e3≻v → (x3,s3);
        (T,cs) = the Arr (heap s3 a); obj = Arr T (cs[i↦v]);
        x3'= raise if (¬G,heap s3 ⊢ v fits T) ArrStore
            (raise if (cs i = None) IndOutBound (np a' x3)) ]] ⟹
                          G ⊢ Norm s0 −(e1[e2]:=e3)≻v→ c hupd[a↦obj](x3',s3)"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
Call  "[[ G ⊢ Norm s0  −e≻a'→ s1;
        G ⊢  s1  −p≻pv→ (x2,(h,l)); dynT = fst(the Obj (h (the Addr a')));
        (md,(pn,rT),lvars,blk,res) = the (cmethd G dynT (mn,pT));
        G ⊢ (np a' x2,(h,init vars lvars[This↦a'][pn↦pv])) −blk→s3;
        G ⊢  s3 −res≻v → (x4,s4) ]] ⟹
                        G ⊢ Norm s0 −(e..mn{pT}(p))≻v→ (x4,(heap s4,l))"

(* execution of statements *)
(* cf. 14.1 *)
XcptS                           "G ⊢ (Some xc,s) −c→ (Some xc,s)"
(* allocation of exception object for system exceptions *)
SXcpt "[[ G ⊢ Norm s0 −c→ (Some (SysXcpt xn),s1);
        new Addr (heap s1) = Some (a,x);
        xobj = init Obj G (SXcpt (if x = None then xn else OutOfMemory)) ]] ⟹
               G ⊢ Norm s0 −c→ (Some (XcptLoc a),hupd[a↦xobj]s1)"
(* cf. 14.5 *)
Skip                              "G ⊢ Norm s −Skip→ Norm s"
(* cf. 14.7 *)
Expr  "[[ G ⊢ Norm s0 −e≻v→ s1 ]] ⟹
                                G ⊢ Norm s0 −Expr e→ s1"
(* cf. 14.2 *)
Comp  "[[ G ⊢ Norm s0 −c1 → s1;
        G ⊢  s1 −c2 → s2 ]] ⟹
                             G ⊢ Norm s0 −(c1;; c2)→ s2"

(* cf. 14.8.2 *)
Cond  "[[ G ⊢ Norm s0 −e≻v→ s1;
        G ⊢  s1−(if the Bool v then c1 else c2)→ s2 ]] ⟹
                    G ⊢ Norm s0 −(If(e) c1 Else c2)→ s2"
(* cf. 14.10, 14.10.1 *)
Loop  "[[ G ⊢ Norm s0 −(If(e) (c;; While(e) c) Else Skip)→ s1 ]] ⟹
                          G ⊢ Norm s0 −(While(e) c)→ s1"
(* cf. 14.16 *)
Throw "[[ G ⊢ Norm s0 −e≻a'→ (x1,s1); x1' = np a' x1;
        x1''=(if x1'=None then (Some (XcptLoc (the Addr a'))) else x1') ]] ⟹
                               G ⊢ Norm s0 −Throw e→ (x1'',s1)"
(* cf. 14.18.1 *)
Try1  "[[ G ⊢ Norm s0 −c1→ (Some (XcptLoc a),s1);
        G ⊢ xcpt ty s1 (XcptLoc a)⪯Class tn;
        G ⊢ Norm(lupd[vn↦Addr a]s1) −c2→ s2 ]] ⟹
              G ⊢ Norm s0 −(Try c1 Catch(tn vn) c2)→ s2"
Try2  "[[ G ⊢ Norm s0 −c1→ (x1,s1);
        x1=None ∨ x1=Some (XcptLoc a) ∧ ¬G ⊢ xcpt ty s1 (XcptLoc a)⪯Class tn ]] ⟹
              G ⊢ Norm s0 −(Try c1 Catch(tn vn) c2)→ (x1,s1)"
(* cf. 14.18.2 *)
Fin   "[[ G ⊢ Norm s0 −c1 → (x1,s1);
        G ⊢ Norm s1 −c2 → (x2,s2);
        x2' = (if x1 ≠ None ∧ x2 = None then x1 else x2) ]] ⟹
                       G ⊢ Norm s0 −(c1 Finally c2)→ (x2',s2)"

end

(*  Title:      isabelle/Bali/Example.thy
    ID:         $Id: Example.thy,v 1.2 1998/04/08 15:26:59 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
The following Bali example program includes:
 class declarations with inheritance, hiding of fields, and overriding of
  methods (with refined result type),
 instance creation, local assignment, sequential composition,
 try & catch, method call with dynamic binding, literal values,
 expression statement, local access, type cast, field assignment (in part), skip
class Base {
  boolean vee;
  Base foo(Base x) {return x;}

}

class Ext extends Base{
  int vee;
  Ext foo(Base x) {((Ext)x).vee=1; return null;}

}

class Example {
  public static void main (String args[]) {
    Base e;
    e=new Ext();
    try {e.foo(null); }
    catch (NullPointerException x) {}

} }

*)
Example = Eval +
datatype tnam  = Base  | Ext
datatype enam  = vee   | x  | e

consts

  tnam  :: "tnam ⇒ tnam"
  enam  :: "enam ⇒ enam"
rules (* tnam  and enam  are intended to be isomorphic to tnam and enam *)
  inj tnam   "(tnam  x = tnam  y) = (x = y)"
  inj enam   "(enam  x = enam  y) = (x = y)"
  surj tnam  "∃m. n = tnam  m"
  surj enam  "∃m. n = enam  m"

syntax

Base,  Ext    :: tname
vee, x, e     :: ename

translations

"Base" == "TName (tnam  Base )"
"Ext"  == "TName (tnam  Ext )"
"vee"  == "EName (enam  vee )"
"x"    == "EName (enam  x )"
"e"    == "EName (enam  e )"

consts

system classes :: cdecl list
tprg           :: prog
BaseC, ExtC    :: cdecl
test           :: stmt
foo            :: mname
a,b            :: loc

defs

BaseC def     "BaseC ≡ (Base, (Some Object, [],
                              [(vee, PrimT Boolean)],
                              [((foo,Class Base),(x,Class Base),
                                ([],Skip,LAcc x))]))"
ExtC def      "ExtC ≡ (Ext,  (Some Base  , [],
                              [(vee, PrimT Integer)],
                              [((foo,Class Base),(x,Class Ext),
                                ([],Expr(Cast (Class Ext) (LAcc x).{ClassT
                                    Ext}vee:=Lit (Intg ($#1))),Lit Null))]))"
system classes def "system classes ≡ [ObjectC, SXcptC Throwable,
              SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
              SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
tprg def "tprg ≡ ([],system classes@[BaseC,ExtC])"
test def "test ≡ Expr(e:=NewC Ext);;
                 Try Expr(LAcc e..foo{Class Base}(Lit Null))
                 Catch(SXcpt NullPointer x) (Throw (LAcc x))"

NP            :: xname
"classes"     :: cdecl list
obj1, obj2    :: obj
s0,s1,s2,s3,s4,s5,s6,s7:: state

translations

"NP"   == "NullPointer"
"classes" == "[ObjectC, SXcptC Throwable,
               SXcptC NP         , SXcptC OutOfMemory, SXcptC ClassCast,
               SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore ,
               BaseC, ExtC]"
"obj1" == "Obj Ext (empty[(vee, ClassT Base)↦Bool False ]
                         [(vee, ClassT Ext )↦Intg ($# 0)])"
"obj2" == "Obj (SXcpt NP) empty"
"s0" == " Norm              (empty                ,empty)"
"s1" == " Norm              (empty[a↦obj1]        ,empty[e↦Addr a])"
"s2" == " Norm              (empty[a↦obj1]        ,
                                              empty[This↦Addr a][x↦Null])"
"s3" == "(Some (SysXcpt NP), empty[a↦obj1]        ,
                                              empty[This↦Addr a][x↦Null])"
"s4" == "(Some (SysXcpt NP), empty[a↦obj1]        ,empty[e↦Addr a])"
"s5" == "(Some (XcptLoc b ), empty[a↦obj1][b↦obj2],empty[e↦Addr a])"
"s6" == " Norm              (empty[a↦obj1][b↦obj2],empty[e↦Addr a][x↦Addr b])"
"s7" == "(Some (XcptLoc b ), empty[a↦obj1][b↦obj2],empty[e↦Addr a][x↦Addr b])"

end

(*  Title:      isabelle/Bali/Trans.thy
    ID:         $Id: Trans.thy,v 1.10 1998/04/08 15:27:08 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Operational transition (small-step) semantics of the
execution of Java expressions and statements
#####PRELIMINARY!!!!!!!!
improvements over Java Specification 1.0 (cf. 15.11.4.4):
* dynamic method lookup does not need to check the return type
* throw raises a NullPointer exception if a null reference is given, and each
  throw of a system exception yield a fresh exception object (was not specified)
* if there is not enough memory even to allocate an OutOfMemory exception,
  evaluation/execution fails, i.e. simply stops (was not specified)
design issues:
* Lit expressions and Skip statements are considered completely evaluated.
* the expr entry in rules is redundant in case of exceptions, but its full
  inclusion helps to make the rule structure independent of exception occurence.
* the rule format is such that the start state may contain an exception.
  ++ faciliates exception handling (to be added later)
  +  symmetry
* the rules are defined carefully in order to be applicable even in not
  type-correct situations (yielding undefined values),
  e.g. the Adr (Val (Bool b)) = arbitrary.
  ++ fewer rules
  -  less readable because of auxiliary functions like the Adr
  Alternative: "defensive" evaluation throwing some InternalError exception
               in case of (impossible, for correct programs) type mismatches
simplifications:
* just simple handling (i.e. propagation) of exceptions so far
* dynamic method lookup does not check return type (should not be necessary)
*)
Trans = Eval +

consts

  texpr tstmt   :: "prog ⇒ (((expr × state) × (expr × state)) +
                            ((stmt × state) × (stmt × state))) set"
syntax (symbols)
  texpr :: "[prog, expr × state, expr × state] ⇒ bool "(" ⊢ →1  "[51,82,82] 81)
  tstmt :: "[prog, stmt × state, stmt × state] ⇒ bool "(" ⊢ ↦1  "[51,82,82] 81)
  Ref   :: "loc ⇒ expr"
(*sub expr expr :: "(expr ⇒ expr) ⇒ prop"*)

translations

  "G ⊢ e s →1 ex s'" == "Inl (e s, ex s') ∈ texpr tstmt G"
  "G ⊢ s s ↦1 s' s'" == "Inr (s s, s' s') ∈ texpr tstmt G"
  "Ref a" == "Lit (Addr a)"
(*"sub expr expr ef" == "⋀G e0 s e' s'. G ⊢ (   e0,s) →1 (   e',s') ]] ⟹
                                        G ⊢ (ef e0,s) →1 (ef e',s')"*)

inductive "texpr tstmt G" intrs
(* evaluation of expression *)
(* cf. 15.5 *)
XcptE "[[∀v. e ≠ Lit v ]] ⟹
                                G ⊢ (e,Some xc,s) →1 (Lit arbitrary,Some xc,s)"
(* cf. 15.8.1 *)
NewC  "[[ new Addr (heap s) = Some (a,x);
        s' = c hupd[a↦init Obj G C](x,s) ]] ⟹
                              G ⊢ (NewC C,None,s) →1 (Ref a,s')"
(* cf. 15.9.1 *)
(*NewA1 "sub expr expr (NewA T)"*)
NewA1 "[[ G ⊢ (e,None,s) →1 (e',s') ]] ⟹
                            G ⊢ (New T[e],None,s) →1 (New T[e'],s')"
NewA  "[[ i = the Intg i'; new Addr (heap s) = Some (a, x);
        s' = c hupd[a↦init Arr T i](raise if (i<$#0) NegArrSize x,s) ]] ⟹
                      G ⊢ (New T[Lit i'],None,s) →1 (Ref a,s')"
(* cf. 15.15 *)
Cast1 "[[ G ⊢ (e,None,s) →1 (e',s') ]] ⟹
                            G ⊢ (Cast T e,None,s) →1 (Cast T e',s')"
Cast  "[[ x'= raise if (¬G,heap s ⊢ v fits T) ClassCast None ]] ⟹
                      G ⊢ (Cast T (Lit v),None,s) →1 (Lit v,x',s)"
(* cf. 15.7.1 *)
(*Lit                           "G ⊢ (Lit v,None,s) →1 (Lit v,None,s)"*)
(* cf. 15.13.1, 15.2 *)
LAcc  "[[ v = the (locals s vn) ]] ⟹
                             G ⊢ (LAcc vn,None,s) →1 (Lit v,None,s)"
(* cf. 15.25.1 *)
LAss1 "[[ G ⊢ (e,None,s) →1 (e',s') ]] ⟹
                               G ⊢ (vn:=e,None,s) →1 (vn:=e',s')"
LAss                      "G ⊢ (vn:=Lit v,None,s) →1 (Lit v,None,lupd[vn↦v]s)"
(* cf. 15.10.1, 15.2 *)
FAcc1 "[[ G ⊢ (e,None,s) →1 (e',s') ]] ⟹
                             G ⊢ (e.{T}fn,None,s) →1 (e'.{T}fn,s')"
FAcc  "[[ v = the (snd (the Obj (heap s (the Addr a'))) (fn,T)) ]] ⟹
                        G ⊢ (Lit a'.{T}fn,None,s) →1 (Lit v,np a' None,s)"
(* cf. 15.25.1 *)
FAss1 "[[ G ⊢ (e1,None,s) →1 (e1',s') ]] ⟹
                        G ⊢ (e1.{T}fn:=e2,None,s) →1 (e1'.{T}fn:=e2,s')"
FAss2 "[[ G ⊢ (e2,np a' None,s) →1 (e2',s') ]] ⟹
                    G ⊢ (Lit a'.{T}fn:=e2,None,s) →1 (Lit a'.{T}fn:=e2',s')"
FAss  "[[ a = the Addr a'; (c,fs) = the Obj (heap s a);
        s'= c hupd[a↦Obj c (fs[(fn,T)↦v])](None,s) ]] ⟹
                 G ⊢ (Lit a'.{T}fn:=Lit v,None,s) →1 (Lit v,s')"

(* cf. 15.12.1 *)
AAcc1 "[[ G ⊢ (e1,None,s) →1 (e1',s') ]] ⟹
                              G ⊢ (e1[e2],None,s) →1 (e1'[e2],s')"
AAcc2 "[[ G ⊢ (e2,None,s) →1 (e2',s') ]] ⟹
                          G ⊢ (Lit a'[e2],None,s) →1 (Lit a'[e2'],s')"
AAcc  "[[ vo = snd (the Arr (heap s (the Addr a'))) (the Intg i');
        x' = raise if (vo = None) IndOutBound (np a' None) ]] ⟹
                      G ⊢ (Lit a'[Lit i'],None,s) →1 (Lit (the vo),x',s)"
(* cf. 15.25.1 *)
AAss1 "[[ G ⊢ (e1,None,s) →1 (e1',s') ]] ⟹
                          G ⊢ (e1[e2]:=e3,None,s) →1 (e1'[e2]:=e3,s')"
AAss2 "[[ G ⊢ (e2,None,s) →1 (e2',s') ]] ⟹
                      G ⊢ (Lit a'[e2]:=e3,None,s) →1 (Lit a'[e2']:=e3,s')"
AAss3 "[[ G ⊢ (e3,None,s) →1 (e3',s') ]] ⟹
                  G ⊢ (Lit a'[Lit i']:=e3,None,s) →1 (Lit a'[Lit i']:=e3',s')"
AAss  "[[ a = the Addr a'; i = the Intg i'; (T,cs) = the Arr (heap s a);
        x'= raise if (¬G,heap s ⊢ v fits T) ArrStore
                (raise if (cs i = None) IndOutBound (np a' None));
        s'= c hupd[a↦Arr T (cs[i↦v])](x',s) ]] ⟹
                          G ⊢ (e1[e2]:=e3,None,s) →1 (Lit v,s')"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
Call1 "[[ G ⊢ (e,None,s) →1 (e',s') ]] ⟹
                        G ⊢ (e..mn{pT}(p),None,s) →1 (e'..mn{pT}(p),s')"
Call2 "[[ G ⊢ (p,None,s) →1 (p',s') ]] ⟹
                   G ⊢ (Lit a'..mn{pT}(p),None,s) →1 (Lit a'..mn{pT}(p'),s')"
Call  "[[ a = the Addr a'; (md,(pn,rT),lvars,blk,res) =
                         the (cmethd G (fst (the Obj (h a))) (mn,pT)) ]] ⟹
          G ⊢ (Lit a'..mn{pT}(Lit pv),None,(h,l)) →1
            (Body blk res l,np a' x,(h,init vars lvars[This↦a'][pn↦pv]))"
Body1 "[[ G ⊢ (s0,None,s) ↦1 (s0',s') ]] ⟹
                 G ⊢ (Body s0    e      l,None,s) →1 (Body s0'  e  l,s')"
Body2 "[[ G ⊢ (e ,None,s) →1 (e',s') ]] ⟹
                 G ⊢ (Body Skip  e      l,None,s) →1 (Body Skip e' l,s')"
Body            "G ⊢ (Body Skip (Lit v) l,None,s) →1 (Lit v,None,(heap s,l))"
(* execution of statements *)
(* cf. 14.1 *)
XcptS "[[ s0 ≠ Skip ]] ⟹
                               G ⊢ (s0,Some xc,s) ↦1 (Skip,Some xc,s)"
(* cf. 14.5 *)
(*Skip                           "G ⊢ (Skip,None,s) ↦1 (Skip,None,s)"*)
(* cf. 14.2 *)
Comp1 "[[ G ⊢ (s1,None,s) ↦1 (s1',s') ]] ⟹
                             G ⊢ (s1;; s2,None,s) ↦1 (s1';; s2,s')"
Comp                      "G ⊢ (Skip;; s2,None,s) ↦1 (s2,None,s)"

(* cf. 14.7 *)
Expr1 "[[ G ⊢ (e ,None,s) →1 (e',s') ]] ⟹
                              G ⊢ (Expr e,None,s) ↦1 (Expr e',s')"
Expr                   "G ⊢ (Expr (Lit v),None,s) ↦1 (Skip,None,s)"
(* cf. 14.8.2 *)
Cond1 "[[ G ⊢ (e ,None,s) →1 (e',s') ]] ⟹
                    G ⊢ (If(e) s1 Else s2,None,s) ↦1 (If(e') s1 Else s2,s')"
Cond           "G ⊢ (If(Lit v) s1 Else s2,None,s) ↦1
                  (if the Bool v then s1 else s2,None,s)"
(* cf. 14.10, 14.10.1 *)
Loop                    "G ⊢ (While(e) s0,None,s) ↦1
                           (If(e) (s0;; While(e) s0) Else Skip,None,s)"

end 32