theory PreBasis = Main:

hide const In0 In1

end

1 Basis

(*  Title:      isabelle/Bali/Basis.thy
    ID:         $Id: Basis.thy,v 1.28 2000/07/14 14:48:59 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Definitions extending HOL as logical basis of Bali
*)
Basis = PreBasis +
constdefs
          the_Inl  :: "'a + 'b ⇒ 'a"
         "the_Inl x ≡ εa. x = Inl a"
          the_Inr  :: "'a + 'b ⇒ 'b"
         "the_Inr x ≡ εb. x = Inr b"
datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
constdefs
          the_In1  :: "('a, 'b, 'c) sum3 ⇒ 'a"
         "the_In1 x ≡ εa. x = In1 a"
          the_In2  :: "('a, 'b, 'c) sum3 ⇒ 'b"
         "the_In2 x ≡ εb. x = In2 b"
          the_In3  :: "('a, 'b, 'c) sum3 ⇒ 'c"
         "the_In3 x ≡ εc. x = In3 c"
syntax
         In1l   :: "'al ⇒ ('al + 'ar, 'b, 'c) sum3"
         In1r   :: "'ar ⇒ ('al + 'ar, 'b, 'c) sum3"
translations
        "In1l e" == "In1 (Inl e)"
        "In1r c" == "In1 (Inr c)"
translations

  "option"<= (type) "Option.option"
  "list"  <= (type) "List.list"
  "sum3"  <= (type) "Basis.sum3"
syntax
  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
translations
 "fun_sum" == "sum_case"

syntax
  "@Oall" :: [pttrn, 'a option, bool] => bool   ("(3! _:_:/ _)" [0,0,10]
10)
  "@Oex"  :: [pttrn, 'a option, bool] => bool   ("(3? _:_:/ _)" [0,0,10]
10)
syntax (symbols)
  "@Oall" :: [pttrn, 'a option, bool] => bool   ("(3∀ _∈_:/ _)"  [0,0,10]
10)
  "@Oex"  :: [pttrn, 'a option, bool] => bool   ("(3∃ _∈_:/ _)"  [0,0,10]
10)
translations
  "! x:A: P"    == "! x:o2s A. P"
  "? x:A: P"    == "? x:o2s A. P"
constdefs
  unique   :: "('a × 'b) list ⇒ bool"
 "unique ≡ nodups ∘ map fst"
consts
  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
defs
  lsplit_def     "lsplit == %f l. f (hd l) (tl l)"
(*  list patterns -- extends pre-defined type "pttrn" used in abstractions
*)
syntax
  "_lpttrn"    :: [pttrn,pttrn] => pttrn     ("_#/_" [901,900] 900)
translations
  "%y#x#xs. b"  == "lsplit (%y x#xs. b)"
  "%x#xs  . b"  == "lsplit (%x xs  . b)"
syntax

  "@dummy_pat"   :: pttrn    ("'_")
end
ML
fun dummy_pat_tr [] = Free ("_",dummyT)
  | dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts);
val parse_translation = ("@dummy_pat", dummy_pat_tr)::parse_translation;

2 Name

(*  Title:      isabelle/Bali/Name.thy
    ID:         $Id: Name.thy,v 1.5 2000/06/29 19:35:31 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Java names
simplifications:
no packages, thus no internal structure of names
*)
Name = Basis +
(* cf. 6.5 *)
types   tnam            (* ordinary type name, i.e. class or interface
name *)
        ename           (* expression name, i.e. variable or field name
*)
        mname           (* method name *)
arities tnam, ename, mname :: term
types    lname           (* names for local variables and the This pointer
*)
        = "ename + unit"
syntax   EName, This :: lname
translations
  "lname" <= (type) "ename + unit"
  "EName" => "Inl"
  "This"  => "Inr ()"

datatype xname          (* names of standard exceptions *)
        = Throwable
        | NullPointer | OutOfMemory | ClassCast
        | NegArrSize  | IndOutBound | ArrStore
datatype tname          (* type names for standard classes and other type
names *)
        = Object
        | SXcpt   xname
        | TName   tnam
translations
  "mname" <= (type) "Name.mname"
  "xname" <= (type) "Name.xname"
  "tname" <= (type) "Name.tname"
  "ename" <= (type) "Name.ename"
end

3 Type

(*  Title:      isabelle/Bali/Type.thy
    ID:         $Id: Type.thy,v 1.19 2000/05/02 09:40:54 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Java types
simplifications:
* only the most important primitive types
* the null type is regarded as reference type
*)
Type = Name +
datatype prim_ty        (* primitive type, cf. 4.2 *)
        = Void          (* 'result type' of void methods *)
        | Boolean
        | Integer

datatype ref_ty         (* reference type, cf. 4.3 *)
        = NullT         (* null type, cf. 4.1 *)
        | IfaceT tname  (* interface type *)
        | ClassT tname  (* class type *)
        | ArrayT ty     (* array type *)
and ty                  (* any type, cf. 4.1 *)
        = PrimT prim_ty (* primitive type *)
        | RefT  ref_ty  (* reference type *)
translations
  "prim_ty" <= (type) "Type.prim_ty"
  "ref_ty"  <= (type) "Type.ref_ty"
  "ty"      <= (type) "Type.ty"
syntax
         NT     :: "          ty"
         Iface  :: "tname ⇒ ty"
         Class  :: "tname ⇒ ty"
         Array  :: "ty  ⇒ ty"   ("_.[]" [90] 90)
translations
        "NT"      == "RefT   NullT"
        "Iface I" == "RefT (IfaceT I)"
        "Class C" == "RefT (ClassT C)"
        "T.[]"    == "RefT (ArrayT T)"
constdefs
  the_Class :: "ty ⇒ tname"
 "the_Class T ≡ εC. T = Class C"
end

4 Value

(*  Title:      isabelle/Bali/Value.thy
    ID:         $Id: Value.thy,v 1.3 2000/07/14 14:48:59 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Java values
*)

Value = Type +
types   loc             (* locations, i.e. abstract references on objects
*)
arities loc :: term
datatype val_(** name not 'val' because of nasty clash with ML token
'val' **)
        = 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_"
             "val" <= (type) "Term.val_"
             "loc" <= (type) "Term.loc"
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"
types   dyn_ty      = "loc ⇒ ty option"
consts
  typeof        :: "dyn_ty ⇒ val ⇒ ty option"
  defpval       :: "prim_ty ⇒ val"      (* default value for primitive
types *)
  default_val   :: "     ty ⇒ val"      (* default value for all types
*)
primrec "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"
primrec "defpval Void    = Unit"
        "defpval Boolean = Bool False"
        "defpval Integer = Intg #0"
primrec "default_val (PrimT pt) = defpval pt"
        "default_val (RefT  r ) = Null"

end

5 Term

(*  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 ⇒  expr" ("!!")
LAss :: "ename ⇒ expr ⇒ 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 ⇒ bool"
"is_stmt t ≡ ∃ c. t=In1r c"
end

6 Table

(*  Title:      isabelle/Bali/Table.thy
ID:         $Id: Table.thy,v 1.25 2000/06/29 19:35:31 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 standard, 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)
  -  sometimes 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 *)
  table_sum_cond:: "('a, 'c) table ⇒ bool ⇒ 'c ⇒ ('a + unit, 'c)
table"

                                           ("_'(+')¬_?↦_" [81, 50,

80] 80)
translations
  "table_of"  == "map_of"
  "m (+)¬b ?↦c" == "m (+) (if b then empty else empty(()↦c))"
  (type)"'a ⇝ 'b"       <= (type)"'a ⇒ 'b Option.option"

  (type)"('a, 'b) table" <= (type)"'a ⇝ 'b"
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: ∀ y∈s k:
R x y"
end

7 Decl

(*  Title:      isabelle/Bali/Decl.thy
    ID:         $Id: Decl.thy,v 1.38 2000/07/25 21:54:10 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Field, method, interface, and class declarations, whole Java programs
simplifications:
* the only field and method modifier is static
* no constructors, which may be simulated by new + suitable methods
* there is just one global initializer per class, which can simulate all
others
* 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)
* no interface modifiers yet, i.e. every interface is public
* no interface fields
* no class modifiers yet, i.e. every class is public, non-final
* every class has an explicit superclass (unused for Object)
* the (standard) methods of Object and of standard exceptions are not
specified
* no packages
* no main method
*)
Decl = Term + Table + (** order is significant, because of clash for "var"
**)
types   modi = bool     (* modifier: static *)
        field
        = "modi × ty"
        fdecl           (* field declaration, cf. 8.3 *)
        = "ename × field"
translations
  "field" <= (type) "bool × ty"
  "fdecl" <= (type) "ename × field"
types (*sig: see Term.thy *)
        mhead           (* method head (excluding signature) *)
        = "modi × ename list × ty"
        (* modifier, parameter names, result type *)
        mbody           (* method body *)
        = "(ename × ty) list × stmt × expr"
        (* local variables, block+result expression *)
        methd           (* method in a class *)
        = "mhead × mbody"

mdecl           (* method declaration in a class *)
= "sig × methd"
translations
"mhead" <= (type) "bool × ename list × ty"
"mbody" <= (type) "(ename × ty) list × stmt × expr"
"methd" <= (type) "mhead × mbody"
"mdecl" <= (type) "sig × methd"
syntax
static    :: "modi ⇒ bool"
mrt       :: "mhead ⇒ ty"
translations
"static"       => "id"
"mrt mh"       => "snd (snd mh)"

types   ibody           (* interface body *)
= "(sig × mhead) list"
(* methods *)
iface           (* interface *)
= "tname list × ibody"
(* superinterface list *)
idecl           (* interface declaration, cf. 9.1 *)
= "tname × iface"
translations
"ibody" <= (type) "(sig × mhead) list"
"iface" <= (type) "tname list × ibody"
"idecl" <= (type) "tname × iface"

types   cbody           (* class body *)
= "fdecl list × mdecl list × stmt"
(* fields, methods, initializer *)
class           (* class *)
= "tname × tname list × cbody"
(* superclass, implemented interfaces *)

        cdecl           (* class declaration, cf. 8.1 *)
        = "tname × class"
translations
  "cbody" <= (type) "fdecl list × mdecl list × stmt"
  "class" <= (type) "tname × tname list × cbody"
  "cdecl" <= (type) "tname × class"
consts
  Object_mdecls  :: "mdecl list" (* methods of Object *)
  SXcpt_mdecls   :: "mdecl list" (* methods of SXcpts *)
  ObjectC ::        "cdecl"      (* declaration  of root      class   *)
  SXcptC  ::"xname ⇒ cdecl"      (* declarations of throwable classes
*)
  standard_classes :: cdecl list
defs
ObjectC_def "ObjectC ≡ (Object  , (arbitrary      ,[],[],Object_mdecls,Skip))"
SXcptC_def  "SXcptC xn≡ (SXcpt xn, (if xn = Throwable then Object else
                                     SXcpt Throwable,[],[],SXcpt_mdecls,Skip))"
standard_classes_def "standard_classes ≡ [ObjectC, SXcptC Throwable,
                SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
                SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"

(* programs *)
types prog  =        "idecl list × cdecl list"
translations
     "prog"<= (type) "idecl list × cdecl list"
syntax
  iface     :: "prog ⇒ (tname, iface) table"
  class     :: "prog ⇒ (tname, class) table"
  is_iface  :: "prog ⇒ tname ⇒ bool"
  is_class  :: "prog ⇒ tname ⇒ bool"
translations
           "iface G I" == "table_of (fst G) I"
           "class G C" == "table_of (snd G) C"
        "is_iface G I" == "iface G I ≠ None"
        "is_class G C" == "class G C ≠ None"

consts
  is_type :: "prog ⇒  ty ⇒ bool"
  isrtype :: "prog ⇒ ref_ty ⇒ bool"
primrec "is_type G (PrimT pt)  = True"
        "is_type G (RefT  rt)  = isrtype G rt"
        "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"

(* subinterface and subclass relation, in anticipation of TypeRel.thy
*)
consts
  subint1,
  subcls1  :: "prog ⇒ (tname × tname) set"
defs
  subint1_def   "subint1 G ≡ {(I,J). ∃ i∈iface G I: J∈set (fst i)}"
  subcls1_def   "subcls1 G ≡ {(C,D). C≠Object ∧ (∃ c∈class G C: fst
c = D)}"
(* well-structured programs *)
constdefs
  ws_idecl :: "prog ⇒ tname ⇒ tname list ⇒ bool"
 "ws_idecl G I si ≡ ∀ J∈set si.  is_iface G J ∧ (J,I)∉(subint1 G)^+"
  ws_cdecl :: "prog ⇒ tname ⇒ tname ⇒ bool"
 "ws_cdecl G C sc ≡ C≠Object ⟶ is_class G sc ∧ (sc,C)∉(subcls1 G)^+"
  ws_prog  :: "prog ⇒ bool"
 "ws_prog G ≡ (∀ (I,(si,ib))∈set (fst G). ws_idecl G I si) ∧
              (∀ (C,(sc,cb))∈set (snd G). ws_cdecl G C sc)"
(* auxiliary well-founded relation for the recursion operators below *)
constdefs
  ws_wfrel :: "(prog ⇒ (tname × tname) set) ⇒
               ((prog × tname) × (prog × tname)) set"
 "ws_wfrel R ≡ {((G,I),(G',I')). G' = G ∧ ws_prog G ∧ (I',I) ∈ R G}"
(* general operators for recursion over the interface and class hiearchies

*)
consts
  iface_rec   :: "prog × tname ⇒  (tname ⇒ ibody ⇒ 'a set ⇒
'a) ⇒ 'a"
  class_rec   :: "prog × tname ⇒ 'a ⇒ (tname ⇒ cbody ⇒ 'a  ⇒
'a) ⇒ 'a"
recdef iface_rec "ws_wfrel subint1" congs image_cong
"iface_rec (G,I) = (λf. case iface G I of None ⇒ arbitrary | Some (si,ib)

⇒

                    if ws_prog G then f I ib ((λJ. iface_rec (G,J) f)``set
si)
                    else arbitrary)"
recdef class_rec "ws_wfrel subcls1"
"class_rec(G,C) = (λt f. case class G C of None⇒ arbitrary | Some (sc,si,cb)⇒
       if ws_prog G then f C cb (if C = Object then t else class_rec (G,sc)
t f)
       else arbitrary)"
types
  fspec = "ename × tname"
consts
  imethds       :: "prog ⇒ tname ⇒ ( sig   , tname × mhead) tables"
  cmethd        :: "prog ⇒ tname ⇒ ( sig   , tname × methd) table"
  fields        :: "prog ⇒ tname ⇒ ((ename × tname) × field) list"
  cfield        :: "prog ⇒ tname ⇒ ( ename , tname × field) table"
defs
  (* methods of an interface, with overriding and inheritance, cf. 9.2
*)
  imeths_def "imethds G I ≡ iface_rec (G,I)       (λI     ms      ts.
       (Un_tables ts) ⊕⊕ (o2s ∘ table_of (map (λ(s,m). (s,I,m)) ms)))"
  (* methods of a class, with inheritance, overriding and hiding, cf.
8.4.6 *)
  cmethd_def "cmethd  G C ≡ class_rec (G,C) empty (λC (fs,ms,ini) ts.
                             ts ⊕ table_of (map (λ(s,m). (s,C,m)) ms))"
  (* list of fields of a class, including inherited and hidden ones *)
  fields_def "fields G C ≡ class_rec (G,C) []    (λC (fs,ms,ini) ts.
                                             map (λ(n,t). ((n,C),t)) 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))"

constdefs
  is_methd :: "prog ⇒ tname ⇒ sig ⇒ bool"
 "is_methd G ≡ λC sig. is_class G C ∧ cmethd G C sig ≠ None"
end

8 TypeRel

(*  Title:      isabelle/Bali/TypeRel.thy
    ID:         $Id: TypeRel.thy,v 1.31 2000/07/25 21:54:10 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
The relations between Java types
simplifications:
* subinterface, subclass and widening relation includes identity
improvements over Java Specification 1.0:
* narrowing reference conversion also in cases where the return types
of a pair
  of methods common to both types are in widening (rather identity) relation
* one could add similar constraints also for other cases
design issues:
* the type relations do not require is_type for their arguments
* the subint1 and subcls1 relations imply is_iface/is_class for their
first
  arguments, which is required for their finiteness
*)
TypeRel = Decl +
consts

(*subint1, in Decl.thy*)                    (* direct subinterface   *)
(*subint,  by translation*)                (*        subinterface   *)
(*subcls1, in Decl.thy*)                    (* direct subclass       *)
(*subcls,  by translation*)                (*        subclass       *)
  implmt1,                                   (* direct implementation
*)
  implmt   :: "prog ⇒ (tname × tname) set"(*        implementation *)
  widen,                                    (*        widening       *)
  narrow,                                    (*        narrowing      *)
  cast     :: "prog ⇒ (ty  × ty   ) set"(*        casting        *)
syntax
 "@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)
 "@narrow"  :: "prog => [ty   , ty   ] => bool" ("_|-_:>_"   [71,71,71]
70)
 "@cast"    :: "prog => [ty   , ty   ] => bool" ("_|-_<=:? _"[71,71,71]
70)
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]

"@implmt"  :: "prog ⇒ [tname, tname] ⇒ bool" ("_⊢_⇝_"   [71,71,71]
70)
"@widen"   :: "prog ⇒ [ty   , ty   ] ⇒ bool" ("_⊢_⪯_"    [71,71,71]
70)
"@narrow"  :: "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) ∈(subint1 G)^*" (* cf. 9.1.3 *)
      "G⊢C ≺C1 D" == "(C,D) ∈ subcls1 G"
      "G⊢C ⪯C  D" == "(C,D) ∈(subcls1 G)^*" (* cf. 8.1.3 *)
      "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) ∈ narrow  G"
      "G⊢S ⪯?  T" == "(S,T) ∈ cast    G"

defs
(* direct subinterface in Decl.thy, cf. 9.1.3 *)
(* direct subclass     in Decl.thy, cf. 8.1.3 *)
(* direct implementation, cf. 8.1.3 *)
implmt1_def "implmt1 G≡{(C,I). C≠Object ∧ (∃ c∈class G C: I∈set (fst(snd
c)))}"

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. kind of syntactic subtyping *)
refl                      "G⊢  T⪯T" (*identity conversion, cf.

5.1.1 *)
subint  "G⊢I⪯I J  ⟹ G⊢ Iface I⪯ Iface J"(*wid.ref.conv.,
cf. 5.1.4 *)
int_obj                 "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                    "G⊢  NT⪯ RefT R"
arr_obj                 "G⊢  T.[]⪯ Class Object"
array   "G⊢RefT S⪯RefT T ⟹ G⊢RefT S.[]⪯ RefT T.[]"

(* all properties of narrowing and casting conversions we actually need
*)
(* these can easily be proven from the definitions below *)
(**
rules
cast_RefT2   "G⊢S⪯? RefT R ⟹ ∃ t. S=RefT t"
cast_PrimT2  "G⊢S⪯? PrimT pt ⟹ ∃ t. S=PrimT t ∧ G⊢PrimT t⪯PrimT
pt"
**)
constdefs
widens :: "prog ⇒ [ty list, ty list] ⇒ bool" ("_⊢_[⪯]_" [71,71,71]
70)
"G⊢Ts[⪯]Ts' ≡ list_all2 (λT T'. G⊢T⪯T') Ts Ts'"
(** more detailed than necessary for type-safety, see above rules. *)
inductive "narrow G" intrs (* narrowing reference conversion, cf. 5.1.5
*)
subcls "G⊢C⪯C D  ⟹ G⊢  Class D≻Class C"
implmt "¬G⊢C⇝I  ⟹ G⊢  Class C≻Iface I"
obj_arr                  "G⊢Class Object≻T.[]"
int_cls                  "G⊢  Iface I≻Class C"
subint "imethds G I hidings imethds G J entails
        (λ(md, mh   ) (md',mh').  G⊢mrt mh⪯mrt mh') ⟹
        ¬G⊢I⪯I J  ⟹ G⊢  Iface I≻Iface J"
array  "G⊢RefT S≻RefT T  ⟹ G⊢ RefT S.[]≻RefT T.[]"

inductive "cast G" intrs (* casting conversion, cf. 5.5 *)
widen   "G⊢S⪯T ⟹ G⊢S⪯? T"
narrow  "G⊢S≻T ⟹ G⊢S⪯? T"

end

9 WellType

(*  Title:      isabelle/Bali/WellType.thy
    ID:         $Id: WellType.thy,v 1.42 2000/07/11 20:28:42 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Well-typedness of Java programs
improvements over Java Specification 1.0:
* methods of Object can be called upon references of interface or array
type
simplifications:
* the type rules include all static checks on statements and expressions,
e.g.
  definedness of names (of parameters, locals, fields, methods)
design issues:
* unified type judgment for statements, variables, expressions, expression
lists
* statements are typed like expressions with dummy type Void
* 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
        = "(lname, ty) table"   (* local variables, including This *)
        env
        = "prog × lenv"         (* program, locals *)
syntax
  prg     :: "env ⇒ prog"

  lcl     :: "env ⇒ lenv"
translations
  "lenv" <= (type) "(lname, ty) table"
   "env" <= (type) "prog × lenv"
  "prg"   => "fst"
  "lcl"   => "snd"
types
  emhead = "ref_ty × mhead"
consts
 cmheads :: "prog ⇒ tname ⇒ sig ⇒ emhead set"
  mheads :: "prog ⇒ ref_ty ⇒ sig ⇒ emhead set"
defs
 cmheads_def
"cmheads G C ≡ λsig. (λ(C,(h,b)). (ClassT C,h)) `` o2s (cmethd G C sig)"
primrec
"mheads G   NullT    = (λsig. {})"
"mheads G (IfaceT I) = (λsig. (λ(I,h).(IfaceT I,h)) `` imethds G I sig

∪

                       cmheads G Object sig)"
"mheads G (ClassT C) = cmheads G C"
"mheads G (ArrayT T) = cmheads G Object"
(** more detailed than necessary for type-safety, see below. *)
constdefs
  (* applicable methods, cf. 15.11.2.1 *)
  appl_methds   :: "prog ⇒ ref_ty ⇒ sig ⇒ (emhead × ty list)   set"
 "appl_methds G rt ≡ λ(mn, pTs). {(mh,pTs') |mh pTs'.
                                   mh ∈ mheads G rt (mn, pTs') ∧ G⊢pTs[⪯]pTs'}"
  (* more specific methods, cf. 15.11.2.2 *)
  more_spec     :: "prog ⇒ emhead × ty list ⇒ emhead × ty list ⇒
bool"
 "more_spec G ≡ λ(mh,pTs). λ(mh',pTs'). G⊢pTs[⪯]pTs'"
(*more_spec G ≡λ((d,h),pTs). λ((d',h'),pTs'). G⊢RefT d⪯RefT d'∧G⊢pTs[⪯]pTs'*)
  (* maximally specific methods, cf. 15.11.2.2 *)
   max_spec     :: "prog ⇒ ref_ty ⇒ sig ⇒ (emhead × ty list)   set"
 " max_spec G rt sig ≡{m. m ∈appl_methds G rt sig ∧
                        (∀ m'∈appl_methds G rt sig. more_spec G m' m ⟶
m'=m)}"
(**

rules (* all properties of more_spec, appl_methods and max_spec we actually
need
         these can easily be proven from the above definitions *)
max_spec2mheads "max_spec G rt (mn, pTs) = insert (mh, pTs') A ⟹
      mh∈mheads G rt (mn, pTs') ∧ G⊢pTs[⪯]pTs'"
*)
constdefs
  empty_dt :: "dyn_ty"
 "empty_dt ≡ λa. None"
  invmode :: "modi ⇒ expr ⇒ inv_mode"
 "invmode m e ≡ if static m then Static else if e=Super then SuperM else
IntVir"
types tys  =        "ty + ty list"
translations
  "tys"   <= (type) "ty + ty list"
consts
  wt    :: "(env × dyn_ty × term × tys) set"
(*wt    :: " env ⇒ dyn_ty ⇒ (term × tys) set" not feasible because
of
                                                  changing env in Try
stmt *)
syntax
wt      :: "env ⇒ dyn_ty ⇒ [term,tys] ⇒ bool" ("_,_|=_::_" [51,51,51,51]
50)
wt_stmt :: "env ⇒ dyn_ty ⇒ stmt  ⇒ bool" ("_,_|=_:<>" [51,51,51
] 50)
ty_expr :: "env ⇒ dyn_ty ⇒ [expr ,ty ] ⇒ bool" ("_,_|=_:-_" [51,51,51,51]
50)
ty_var  :: "env ⇒ dyn_ty ⇒ [var  ,ty ] ⇒ bool" ("_,_|=_:=_" [51,51,51,51]
50)
ty_exprs:: "env ⇒ dyn_ty ⇒ [expr list,
                                ty   list] ⇒ bool" ("_,_|=_:#_" [51,51,51,51]
50)
syntax (xsymbols)
wt      :: "env ⇒ dyn_ty ⇒ [term,tys] ⇒ bool" ("_,_⊧_::_"  [51,51,51,51]
50)
wt_stmt :: "env ⇒ dyn_ty ⇒ stmt  ⇒ bool" ("_,_⊧_::√"  [51,51,51

ty_expr :: "env ⇒ dyn_ty ⇒ [expr ,ty ] ⇒ bool" ("_,_⊧_::-_" [51,51,51,51]
50)
ty_var  :: "env ⇒ dyn_ty ⇒ [var  ,ty ] ⇒ bool" ("_,_⊧_::=_" [51,51,51,51]
50)
ty_exprs:: "env ⇒ dyn_ty ⇒ [expr list,
                                ty   list] ⇒ bool"("_,_⊧_::≐_" [51,51,51,51]
50)
translations
        "E,dt⊧t::T" == "(E,dt,t,T) ∈ wt"
        "E,dt⊧s::√"  == "E,dt⊧In1r s::Inl (PrimT Void)"
        "E,dt⊧e::-T" == "E,dt⊧In1l e::Inl T"
        "E,dt⊧e::=T" == "E,dt⊧In2  e::Inl T"
        "E,dt⊧e::≐T" == "E,dt⊧In3  e::Inr T"
syntax (* for purely static typing *)
  wt_:: "env ⇒ [term,tys] ⇒ bool" ("_|-_::_" [51,51,51] 50)
  wt_stmt_:: "env ⇒ stmt  ⇒ bool" ("_|-_:<>" [51,51   ] 50)
  ty_expr_:: "env ⇒ [expr ,ty ] ⇒ bool" ("_|-_:-_" [51,51,51] 50)
  ty_var_:: "env ⇒ [var  ,ty ] ⇒ bool" ("_|-_:=_" [51,51,51] 50)
  ty_exprs_:: "env ⇒ [expr list,
                        ty   list] ⇒ bool" ("_|-_:#_" [51,51,51] 50)
syntax (xsymbols)
  wt_:: "env ⇒ [term,tys] ⇒ bool" ("_⊢_::_"  [51,51,51] 50)
  wt_stmt_::  "env ⇒ stmt  ⇒ bool" ("_⊢_::√"  [51,51   ] 50)
  ty_expr_:: "env ⇒ [expr ,ty ] ⇒ bool" ("_⊢_::-_" [51,51,51] 50)
  ty_var_:: "env ⇒ [var  ,ty ] ⇒ bool" ("_⊢_::=_" [51,51,51] 50)
  ty_exprs_:: "env ⇒ [expr list,
                        ty   list] ⇒ bool" ("_⊢_::≐_" [51,51,51] 50)
translations
        "E⊢t:: T" == "E,empty_dt⊧t:: T"
        "E⊢s::√" == "E,empty_dt⊧s::√"
        "E⊢e::-T" == "E,empty_dt⊧e::-T"
        "E⊢e::=T" == "E,empty_dt⊧e::=T"
        "E⊢e::≐T" == "E,empty_dt⊧e::≐T"
inductive wt 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 *)
If    "[[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⊢tn⪯C SXcpt Throwable]] ⟹
                                       E,dt⊧Throw e::√"
(* cf. 14.18 *)
Try   "[[E,dt⊧c1::√; prg E⊢tn⪯C SXcpt Throwable;
        lcl E (EName vn)=None; (prg E,lcl E(EName 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::√"
Init  "[[is_class (prg E) C]] ⟹
                                       E,dt⊧init C::√"

(* 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; is_type (prg E) T';
        prg E⊢T⪯? T']] ⟹
                                       E,dt⊧Cast T' e::-T'"
(* cf. 15.19.2 *)
Inst  "[[E,dt⊧e::-RefT T;
        prg E⊢RefT T⪯? RefT T']] ⟹
                                       E,dt⊧e InstOf T'::-PrimT Boolean"
(* cf. 15.7.1 *)
Lit   "[[typeof dt x = Some T]] ⟹
                                       E,dt⊧Lit x::-T"
(* cf. 15.10.2, 15.11.1 *)
Super "[[lcl E This = Some (Class C); C ≠ Object;
        class (prg E) C = Some (D, rest)]] ⟹
                                       E,dt⊧Super::-Class D"
(* cf. 15.13.1, 15.10.1, 15.12 *)
Acc   "[[E,dt⊧va::=T]] ⟹
                                       E,dt⊧Acc va::-T"
(* cf. 15.25, 15.25.1 *)
Ass   "[[E,dt⊧va::=T; va ≠ LVar This;
        E,dt⊧v ::-T';

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

(* cf. 15.24 *)
Cond  "[[E,dt⊧e0::-PrimT Boolean;
        E,dt⊧e1::-T1; E,dt⊧e2::-T2;
        prg E⊢T1⪯T2 ∧ T = T2 ∨ prg E⊢T2⪯T1 ∧ T = T1]] ⟹
                                       E,dt⊧e0 ? e1 : e2::-T"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
Call  "[[E,dt⊧e::-RefT t;
        E,dt⊧ps::≐pTs;
        max_spec (prg E) t (mn, pTs) = {((md,(m,pns,rT)),pTs')}]] ⟹
                               E,dt⊧{t,md,invmode m e}e..mn({pTs'}ps)::-rT"

Methd "[[is_class (prg E) C;
        cmethd (prg E) C sig = Some (md,mh,lvars,blk,res);
        E,dt⊧Body md blk res::-T]] ⟹
                                       E,dt⊧Methd C sig::-T"
Body  "[[is_class (prg E) D;
        E,dt⊧blk::√;

        E,dt⊧res::-T]] ⟹

                                       E,dt⊧Body D blk res::-T"
(* well-typed variables *)
(* cf. 15.13.1 *)
LVar  "[[lcl E vn = Some T; is_type (prg E) T]] ⟹
                                       E,dt⊧LVar vn::=T"
(* cf. 15.10.1 *)
FVar  "[[E,dt⊧e::-Class C;
        cfield (prg E) C fn = Some (fd,(m,fT))]] ⟹
                                       E,dt⊧{fd,static m}e..fn::=fT"
(* cf. 15.12 *)
AVar  "[[E,dt⊧e::-T.[];
        E,dt⊧i::-PrimT Integer]] ⟹

                                       E,dt⊧e.[i]::=T"

(* well-typed expression lists *)
(* cf. 15.11.??? *)
Nil                                   "E,dt⊧[]::≐[]"
(* cf. 15.11.??? *)
Cons  "[[E,dt⊧e ::-T;
        E,dt⊧es::≐Ts]] ⟹
                                       E,dt⊧e#es::≐T#Ts"
end

10 WellForm

(*  Title:      isabelle/Bali/WellForm.thy
  ID:         $Id: WellForm.thy,v 1.31 2000/09/11 19:29:05 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 inherits more than one method with the same signature,
the
  methods need not have identical return types
simplifications:
* Object and standard exceptions are assumed to be declared like normal
classes
*)
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,(m,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,pTs) (m,pns,rT). length pTs = length
pns ∧
                               ( ∀ T∈set pTs. is_type G T) ∧ is_type
G rT ∧
                               nodups pns"

wf_mdecl_def  "wf_mdecl G C ≡ λ((mn,pTs),(m,pns,rT),lvars,blk,res).
 wf_mhead G        (mn,pTs) (m,pns,rT) ∧ unique lvars

∧

(C=Object ⟶ ¬static m) ∧ (∀ (vn,T)∈set lvars. is_type
G T) ∧
(∀ pn∈set pns. table_of lvars pn = None) ∧
(∃ T. (G,table_of lvars(pns[↦]pTs) (+)¬static m ?↦Class
C)⊢
     Body C blk res::-T ∧ G⊢T⪯rT)"
(* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
wf_idecl_def  "wf_idecl G ≡ λ(I,(si,ms)). ws_idecl G I si ∧
 ¬is_class G I ∧
(∀ (sig,mh)∈set ms. wf_mhead G sig mh ∧ ¬static (fst
mh)) ∧
unique ms ∧
(o2s ∘ table_of ms hidings Un_tables((λJ.(imethds G J))``set
si)
 entails (λmh (md,mh'). G⊢mrt mh⪯mrt mh'))"
(* 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,init)).
¬is_iface G C ∧
(∀ I∈set si. is_iface G I ∧
     (∀ s. ∀ (md', mh'   ) ∈ imethds G I s.
         (∃ (md ,(mh ,b)) ∈ cmethd  G C s: G⊢mrt mh⪯mrt
mh' ∧
                                          ¬static (fst
mh)))) ∧
(∀ f∈set fs. wf_fdecl G   f) ∧ unique fs ∧
(∀ m∈set ms. wf_mdecl G C m) ∧ unique ms ∧
(G,empty)⊢init::√ ∧ ws_cdecl G C sc ∧
(C ≠ Object ⟶ (table_of ms hiding cmethd G sc entails
                 (λ(mh,b) (md',(mh',b')). G⊢mrt mh⪯mrt
mh' ∧
                          static (fst mh') = static (fst
mh))))"
(* well-formed program, cf. 8.1, 9.1 *)
wf_prog_def   "wf_prog G ≡ let is = fst G; cs = snd G in
        ObjectC ∈ set cs ∧ (∀ xn. SXcptC xn ∈ set cs)

∧

                (∀ i∈set is. wf_idecl G i) ∧ unique is ∧
                (∀ c∈set cs. wf_cdecl G c) ∧ unique cs"
end

11 State

(*  Title:      isabelle/Bali/State.thy
    ID:         $Id: State.thy,v 1.59 2000/08/07 21:07:49 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
State for evaluation of Java expressions and statements
design issues:
* all kinds of objects (class instances, arrays, and class objects)
  are handeled via a general object abstraction
* the heap and the map for class objects are combined into a single table
  (recall (loc, obj) table × (tname, obj) table  ~=  (loc + tname, obj)
table)
simplifications:
*)
State = TypeRel +
datatype  obj_tag =     (* tag for generic object   *)
          CInst tname   (* class instance           *)
        | Arr  ty int   (* array with component type and length *)
     (* | CStat            the tag is irrelevant for a class object,
                           i.e. the static fields of a class *)
types   vn   = "fspec + int"                    (* variable name      *)
        obj  = "obj_tag × (vn, val) table"      (* generalized object
*)
constdefs
  the_Arr :: "obj option ⇒ ty × int × (vn, val) table"
 "the_Arr obj ≡ ε(T,k,t). obj = Some (Arr T k,t)"

upd_obj       :: "vn ⇒ val ⇒ obj ⇒ obj"
"upd_obj n v ≡ λ(oi,vs). (oi,vs(n↦v))"
obj_ty        :: "obj ⇒ ty"
"obj_ty obj  ≡ case fst obj of CInst C ⇒ Class C | Arr T k ⇒ T.[]"
obj_class :: "obj ⇒ tname"
"obj_class obj ≡ case fst obj of CInst C ⇒  C | Arr T k ⇒ Object"

types oref = "loc + tname"          (* generalized object reference *)
syntax
Heap  :: "loc ⇒ oref"
Stat  :: "tname ⇒ oref"
translations
"Heap" => "Inl"
"Stat" => "Inr"
constdefs
fields_table  :: "prog ⇒ tname ⇒ (modi ⇒ bool) ⇒ (fspec, ty) table"
"fields_table G C P ≡ option_map snd ∘ table_of([(fn,(m,fT))∈fields
G C. P m])"
var_tys       :: "prog ⇒ obj_tag ⇒ oref ⇒ (vn, ty) table"
"var_tys G oi r ≡ case r of Heap a ⇒ (case oi of
            CInst C ⇒ fields_table G C (Not ∘ static) (+) empty
          | Arr T k ⇒ empty (+) (λi. if #0≤i∧i<k then Some T else
None))
                         | Stat C ⇒ fields_table G C static (+) empty"

types   globs                  (* global variables: heap and static variables
*)
      = "(oref , obj) table"
      heap
      = "(loc  , obj) table"
      locals
      = "(lname, val) table" (* local variables *)

datatype st = (* pure state, i.e. contents of all variables *)
      st globs locals

constdefs
globs  :: "st ⇒ globs"
"globs ≡ st_case (λg l. g)"
locals :: "st ⇒ locals"
"locals ≡ st_case (λg l. l)"
heap   :: "st ⇒ heap"
"heap s ≡ globs s ∘ Heap"
syntax
val_this     :: "st ⇒ val"
lookup_obj   :: "st ⇒ val ⇒ obj"
translations
"val_this s"       == "the (locals s This)"
"lookup_obj s a'"  == "the (heap s (the_Addr a'))"
syntax
init_vals     :: "('a, ty) table ⇒ ('a, val) table"
translations
"init_vals vs"    == "option_map default_val ∘ vs"
constdefs
gupd       :: "oref ⇒ obj ⇒ st ⇒ st"        ("gupd'(_↦_')"[10,10]1000)
"gupd r obj ≡ st_case (λg l. st (g(r↦obj)) l)"
lupd       :: "lname ⇒ val ⇒ st ⇒ st"        ("lupd'(_↦_')"[10,10]1000)
"lupd vn v ≡ st_case (λg l. st g (l(vn↦v)))"
upd_gobj   :: "oref ⇒ vn ⇒ val ⇒ st ⇒ st"
"upd_gobj r n v ≡ st_case (λg l. st (chg_map (upd_obj n v) r g) l)"
set_locals  :: "locals ⇒ st ⇒ st"
"set_locals l ≡ st_case (λg l'. st g l)"
init_obj    :: "prog ⇒ obj_tag ⇒ oref ⇒ st ⇒ st"
"init_obj G oi r ≡ gupd(r↦(oi, init_vals (var_tys G oi r)))"

syntax
  init_class_obj :: "prog ⇒ tname ⇒ st ⇒ st"
translations
 "init_class_obj G C" == "init_obj G arbitrary (Inr C)"

datatype xcpt           (* exception *)
        = XcptLoc loc   (* location of allocated execption object *)
        | StdXcpt xname (* intermediate standard exception, see Eval.thy
*)
consts
  the_XcptLoc :: "xcpt ⇒ loc"
  the_StdXcpt :: "xcpt ⇒ xname"
defs
  the_XcptLoc_def "the_XcptLoc xc ≡ εa. xc = XcptLoc a"
  the_StdXcpt_def "the_StdXcpt xc ≡ εx. xc = StdXcpt x"
types
  xopt  = "xcpt option"

constdefs
  xcpt_if    :: "bool ⇒ xopt ⇒ xopt ⇒ xopt"
 "xcpt_if c x' x ≡ if c ∧ (x = None) then x' else x"
syntax
  raise_if :: "bool ⇒ xname ⇒ xopt ⇒ xopt"
  np       :: "val  ⇒ xopt ⇒ xopt"
  check_neg:: "val  ⇒ xopt ⇒ xopt"
translations
 "raise_if c xn" == "xcpt_if c (Some (StdXcpt xn))"
 "np v"          == "raise_if (v = Null)      NullPointer"
 "check_neg i'"  == "raise_if (the_Intg i'<0) NegArrSize"
types
  state = "xopt × st"          (* state including exception information

*)
syntax
Norm     :: "st ⇒ state"
translations
"Norm s"     == "(None,s)"
"xopt"       <= (type) "State.xcpt option"
"xopt"       <= (type) "xcpt option"
"state"      <= (type) "xopt × State.st"
"state"      <= (type) "xopt × st"
constdefs
normal     :: "state ⇒ bool"
"normal ≡ λs. fst s = None"
inited   :: "tname ⇒ globs ⇒ bool"
"inited C g ≡ g (Stat C) ≠ None"
initd    :: "tname ⇒ state ⇒ bool"
"initd C ≡ inited C ∘ globs ∘ snd"
xupd     :: "(xopt ⇒ xopt) ⇒ state ⇒ state"
"xupd f ≡ prod_fun f id"
supd     :: "(st ⇒ st) ⇒ state ⇒ state"
"supd ≡ prod_fun id"
syntax
set_lvars     :: "locals ⇒ state ⇒ state"
restore_lvars :: "state ⇒ state ⇒ state"
translations
"set_lvars l" == "supd (set_locals l)"
"restore_lvars s' s" == "set_lvars (locals (snd s')) s"
end

12 Eval

(*  Title:      isabelle/Bali/Eval.thy
    ID:         $Id: Eval.thy,v 1.80 2000/09/13 13:51:58 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Operational evaluation (big-step) semantics of Java expressions and statements
improvements over Java Specification 1.0:
* dynamic method lookup does not need to consider the return type (cf.15.11.4.4)
* throw raises a NullPointer exception if a null reference is given, and
each
  throw of a standard 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)
* array assignment checks lhs (and may throw exceptions) before evaluating
rhs
* fixed exact positions of class initializations (immediate at first active
use)
design issues:
* evaluation vs. (single-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 or stack of invocation frames
     containing local variables and return addresses for method calls
needed
  +  convenient rule induction for subject reduction theorem
  -  no interleaving (for parallelism) can be described
  -  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)
* unified evaluation for variables, expressions, expression lists, statements
* the value entry in statement rules is redundant
* the value entry in rules is irrelevant in case of exceptions, but its
full
  inclusion helps to make the rule structure independent of exception
occurence.
* as irrelevant value entries are ignored, it does not matter if they

are unique
  For simplicity, (fixed) arbitrary values are preferred over "free" values.
* 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_Addr (Val (Bool b)) = arbitrary.
  ++ fewer rules
  -  less readable because of auxiliary functions like the_Addr
  Alternative: "defensive" evaluation throwing some InternalError exception
               in case of (impossible, for correct programs) type mismatches
* there is exactly one rule per syntactic construct
  + no redundancy in case distinctions
* halloc fails iff there is no free heap address. 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.
* the allocation of objects that represent standard exceptions is deferred
until
  execution of any enclosing catch clause, which is transparent to the
program.
  -  requires an auxiliary execution relation
  ++ avoids copies of allocation code and awkward case distinctions (whether
     there is enough memory to allocate the exception) in evaluation rules
* unfortunately new_Addr is not directly executable because of Hilbert
operator.
simplifications:
* local variables are initialized with default values (no definite assignment)
* garbage collection not considered, therefore also no finalizers
* stack overflow and memory overflow during class initialization not modelled
* exceptions in initializations not replaced by ExceptionInInitializerError
*)
Eval = State +
types vvar  =         "val × (val ⇒ state ⇒ state)"
      vals  =        "(val, vvar, val list) sum3"
translations
     "vvar" <= (type) "val × (val ⇒ state ⇒ state)"
     "vals" <= (type)"(val, vvar, val list) sum3"

constdefs
arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 ⇒ vals"
"arbitrary3 ≡ sum3_case (In1 ∘ sum_case (λx. arbitrary) (λx. Unit))
                   (λx. In2 arbitrary) (λx. In3 arbitrary)"
constdefs
throw :: "val ⇒ xopt ⇒ xopt"
"throw a' x ≡ xcpt_if True (Some (XcptLoc (the_Addr a'))) (np a' x)"
fits    :: "prog ⇒ st ⇒ val ⇒ ty ⇒ bool" ("_,_⊢_fits _"[61,61,61,61]60)
"G,s⊢a' fits T ≡ (∃ rt. T=RefT rt) ⟶ a'=Null ∨ G⊢obj_ty(lookup_obj
s a')⪯T"
catch ::"prog ⇒ state ⇒ tname ⇒ bool"      ("_,_⊢catch _"[61,61,61]60)
"G,s⊢catch C≡∃ xc. fst s=Some xc ∧ G,snd s⊢Addr (the_XcptLoc xc) fits
Class C"
new_xcpt_var :: "ename ⇒ state ⇒ state"
"new_xcpt_var vn ≡ λ(x,s). Norm(lupd(EName vn↦Addr (the_XcptLoc (the
x))) s)"
constdefs
assign     :: "('a ⇒ state ⇒ state) ⇒ 'a ⇒ state ⇒ state"
"assign f v ≡ λ(x,s). let (x',s') = (if x = None then f v else id) (x,s)
                 in  (x',if x' = None then s' else s)"
init_comp_ty :: "ty ⇒ stmt"
"init_comp_ty T ≡ if (∃ C. T = Class C) then init (the_Class T) else
Skip"
constdefs
new_Addr   :: "heap ⇒ loc option"
"new_Addr h ≡ if (∀ a. h a ≠ None) then None else Some (εa. h a = None)"
still_free :: "heap ⇒ loc ⇒ bool"
"still_free h a ≡ ∃ b. b ≠ a ∧ h b = None"
enough_mem :: bool
"enough_mem ≡ ∀ h a. new_Addr h = Some a ⟶ still_free h a"

constdefs

  target  :: "inv_mode ⇒ st ⇒ val ⇒ ref_ty ⇒ tname"
 "target m s a' t ≡ if m = IntVir
          then obj_class (lookup_obj s a') else the_Class (RefT t)"
  init_lvars :: "prog ⇒ tname ⇒ sig ⇒ inv_mode ⇒ val ⇒ val list

⇒

                   state ⇒ state"
 "init_lvars G C sig mode a' pvs ≡ λ(x,s). let
              (_,(_,pns,_),lvars,_) = the (cmethd G C sig);
              l = init_vals(table_of lvars)(pns[↦]pvs) (+)¬mode=Static
?↦a'
              in set_lvars l (if mode = Static then x else np a' x,s)"
  body :: "prog ⇒ tname ⇒ sig ⇒ expr"
 "body G C sig ≡ let (D, _, _, c, e) = the (cmethd G C sig) in Body D
c e"
consts
  eval   :: "prog ⇒ (state × term  × vals × state) set"
   halloc:: "prog ⇒ (state × obj_tag × loc × state) set"
  sxalloc:: "prog ⇒ (state  × state) set"
constdefs
  lvar :: "lname ⇒ st ⇒ vvar"
 "lvar vn s ≡ (the (locals s vn), λv. supd (lupd(vn↦v)))"
  fvar :: "tname ⇒ bool ⇒ ename ⇒ val ⇒ state ⇒ vvar × state"
 "fvar C stat fn a' s ≡ let (oref,xf) = if stat then (Stat C,id)
                                        else (Heap (the_Addr a'),np a');
                       n = Inl (fn,C); f = (λv. supd (upd_gobj oref n
v)) in
                  ((the (snd (the (globs (snd s) oref)) n),f),xupd xf
s)"
  avar :: "prog ⇒ val ⇒ val ⇒ state ⇒ vvar × state"
 "avar G i' a' s ≡ let oref = Heap (the_Addr a'); i = the_Intg i'; n
= Inr i;
                       (T,k,cs) = the_Arr (globs (snd s) oref); f = (λv
(x,s).
              (raise_if (¬G,s⊢v fits T) ArrStore x, upd_gobj oref n v
s)) in
       ((the (cs n),f), xupd (raise_if (¬(#0≤i ∧ i<k)) IndOutBound ∘

np a') s)"
syntax
eval ::"[prog,state,term,vals*state]=>bool"("_|-_-_>-> _"  [61,61,80,
61]60)
exec ::"[prog,state,stmt      ,state]=>bool"("_|-_-_-> _"   [61,61,65,
61]60)
evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_-_=>_-> _"[61,61,90,61,61]60)
eval_::"[prog,state,expr ,val, state]=>bool"("_|-_-_->_-> _"[61,61,80,61,61]60)
evals::"[prog,state,expr list ,
                    val  list ,state]=>bool"("_|-_-_#>_-> _"[61,61,61,61,61]60)
hallo::"[prog,state,obj_tag,
                     loc,state]=>bool"("_|-_-halloc _>_-> _"[61,61,61,61,61]60)
sallo::"[prog,state         ,state]=>bool"("_|-_-sxalloc-> _"[61,61,
61]60)
syntax (xsymbols)
eval ::"[prog,state,term,vals×state]⇒bool"("_⊢_−_≻→ _"  [61,61,80,
61]60)
exec ::"[prog,state,stmt      ,state]⇒bool"("_⊢_−_→ _"   [61,61,65,
61]60)
evar ::"[prog,state,var  ,vvar,state]⇒bool"("_⊢_−_=≻_→ _"[61,61,90,61,61]60)
eval_::"[prog,state,expr ,val ,state]⇒bool"("_⊢_−_-≻_→ _"[61,61,80,61,61]60)
evals::"[prog,state,expr list ,
                    val  list ,state]⇒bool"("_⊢_−_≐≻_→ _"[61,61,61,61,61]60)
hallo::"[prog,state,obj_tag,
                     loc,state]⇒bool"("_⊢_−halloc _≻_→ _"[61,61,61,61,61]60)
sallo::"[prog,state,         state]⇒bool"("_⊢_−sxalloc→ _"[61,61,
61]60)
translations
  "G⊢s −t  ≻→ (w,s')" <= "(s,t,   (_args w s')) ∈ eval G"
  "G⊢s −t  ≻→ ws' " == "(s,t,           ws' ) ∈ eval G"
  "G⊢s −c  → (x,s')" <= "G⊢s −In1r c≻→ (In1 Unit,_args x s' )"
  "G⊢s −c  →  s' " == "G⊢s −In1r c≻→ (In1 Unit,        s' )"
  "G⊢s −e-≻v → (x,s')" <= "G⊢s −In1l e≻→ (In1 v   ,_args x s' )"
  "G⊢s −e-≻v →  s' " == "G⊢s −In1l e≻→ (In1 v   ,        s' )"
  "G⊢s −e=≻vf → (x,s')" <= "G⊢s −In2  e≻→ (In2 vf  ,_args x s'
)"
  "G⊢s −e=≻vf →  s' " == "G⊢s −In2  e≻→ (In2 vf  ,        s'
)"
  "G⊢s −e≐≻v → (x,s')" <= "G⊢s −In3  e≻→ (In3 v   ,_args x s'
)"
  "G⊢s −e≐≻v →  s' " == "G⊢s −In3  e≻→ (In3 v   ,        s'

)"
"G⊢s −halloc oi≻a→ (x,s')" <= "(s,oi,a,(_args x s')) ∈ halloc G"
"G⊢s −halloc oi≻a→  s' " == "(s,oi,a,          s') ∈ halloc G"
"G⊢s  −sxalloc→ (x,s')" <= "(s     ,(_args x s')) ∈ sxalloc G"
"G⊢s  −sxalloc→  s' " == "(s     ,          s') ∈ sxalloc G"
inductive "halloc G" intrs (* allocating objects on the heap, cf. 12.5
*)
Xcpt  "G⊢(Some x,s) −halloc oi≻arbitrary→ (Some x,s)"
New   "[[new_Addr (heap s) = Some a;
        (x,oi') = (if still_free (heap s) a then (None,oi)
                   else (Some (XcptLoc a),CInst (SXcpt OutOfMemory)))]]

⟹

        G⊢Norm s −halloc oi≻a→ (x,init_obj G oi' (Heap a) s)"
inductive "sxalloc G" intrs (* allocating exception objects for
                            standard exceptions (other than OutOfMemory)
*)
Norm   "G⊢ Norm              s −sxalloc→ Norm             s"
XcptL  "G⊢(Some (XcptLoc a ),s) −sxalloc→ (Some (XcptLoc a),s)"
SXcpt "[[G⊢Norm s0 −halloc (CInst (SXcpt xn))≻a→ (x,s1)]] ⟹
        G⊢(Some (StdXcpt xn),s0) −sxalloc→ (Some (XcptLoc a),s1)"

inductive "eval G" intrs
(* propagation of exceptions *)
(* cf. 14.1, 15.5 *)
Xcpt  "G⊢(Some xc,s) −t≻→ (arbitrary3 t,(Some xc,s))"

(* execution of statements *)
(* 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 *)
If    "[[G⊢Norm s0 −e-≻b→ s1;
        G⊢  s1−(if the_Bool b then c1 else c2)→ s2]] ⟹
                     G⊢Norm s0 −If(e) c1 Else c2 → s2"
(* cf. 14.10, 14.10.1 *)
(*      G⊢Norm s0 −If(e) (c;; While(e) c) Else Skip→ s3 *)
Loop  "[[G⊢Norm s0 −e-≻b→ s1;
        if the_Bool b then (G⊢s1 −c→ s2 ∧ G⊢s2 −While(e) c→ s3)
                      else s3 = s1]] ⟹
                            G⊢Norm s0 −While(e) c→ s3"
(* cf. 14.16 *)
Throw "[[G⊢Norm s0 −e-≻a'→ s1]] ⟹
                               G⊢Norm s0 −Throw e→ xupd (throw a')
s1"
(* cf. 14.18.1 *)
Try   "[[G⊢Norm s0 −c1→ s1; G⊢s1 −sxalloc→ s2;
        if G,s2⊢catch C then G⊢new_xcpt_var vn s2 −c2→ s3 else s3
= s2]] ⟹
                G⊢Norm s0 −Try c1 Catch(C vn) c2→ s3"
(* cf. 14.18.2 *)
Fin   "[[G⊢Norm s0 −c1→ (x1,s1);
        G⊢Norm s1 −c2→ s2]] ⟹
                 G⊢Norm s0 −c1 Finally c2→ xupd (xcpt_if (x1≠None)
x1) s2"
(* cf. 12.4.2, 8.5 *)
Init  "[[the (class G C) = (sc,si,fs,ms,ini);
        if inited C (globs s0) then s3 = Norm s0
        else (G⊢Norm (init_class_obj G C s0)
                −(if C = Object then Skip else init sc)→ s1 ∧
              G⊢set_lvars empty s1 −ini→ s2 ∧ s3 = restore_lvars
s1 s2)]] ⟹

               G⊢Norm s0 −init C→ s3"

(* evaluation of expressions *)
(* cf. 15.8.1, 12.4.1 *)
NewC  "[[G⊢Norm s0 −init C→ s1;
        G⊢  s1 −halloc (CInst C)≻a→ s2]] ⟹
                                G⊢Norm s0 −NewC C-≻Addr a→ s2"
(* cf. 15.9.1, 12.4.1 *)
NewA  "[[G⊢Norm s0 −init_comp_ty T→ s1; G⊢s1 −e-≻i'→ s2;
        G⊢xupd (check_neg i') s2 −halloc (Arr T (the_Intg i'))≻a→

s3]] ⟹

                              G⊢Norm s0 −New T[e]-≻Addr a→ s3"
(* cf. 15.15 *)
Cast  "[[G⊢Norm s0 −e-≻v→ s1;
        s2 = xupd (raise_if (¬G,snd s1⊢v fits T) ClassCast) s1]] ⟹
                              G⊢Norm s0 −Cast T e-≻v→ s2"
(* cf. 15.19.2 *)
Inst  "[[G⊢Norm s0 −e-≻v→ s1;
        b = (v≠Null ∧ G,snd s1⊢v fits RefT T)]] ⟹
                            G⊢Norm s0 −e InstOf T-≻Bool b→ s1"
(* cf. 15.7.1 *)
Lit                              "G⊢Norm s −Lit v-≻v→ Norm s"

(* cf. 15.10.2 *)
Super                         "G⊢Norm s −Super-≻val_this s→ Norm
s"
(* cf. 15.2 *)
Acc   "[[G⊢Norm s0 −va=≻(v,f)→ s1]] ⟹
                                G⊢Norm s0 −Acc va-≻v→ s1"
(* cf. 15.25.1 *)
Ass   "[[G⊢Norm s0 −va=≻(w,f)→ s1;
        G⊢  s1 −e-≻v → s2]] ⟹
                                 G⊢Norm s0 −va:=e-≻v→ assign f v
s2"

(* cf. 15.24 *)
Cond  "[[G⊢Norm s0 −e0-≻b→ s1;
        G⊢  s1 −(if the_Bool b then e1 else e2)-≻v→ s2]] ⟹
                          G⊢Norm s0 −e0 ? e1 : e2-≻v→ s2"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
Call  "[[G⊢Norm s0 −e-≻a'→ s1; G⊢s1 −args≐≻vs→ s2;
        C = target mode (snd s2) a' cT;
        G⊢init_lvars G C (mn,pTs) mode a' vs s2 −Methd C (mn,pTs)-≻v→

s3]]⟹

        G⊢Norm s0 −{t,cT,mode}e..mn({pTs}args)-≻v→ (restore_lvars
s2 s3)"
Methd "[[G⊢Norm s0 −body G C sig-≻v→ s1]] ⟹
                              G⊢Norm s0 −Methd C sig-≻v→ s1"
(* cf. 14.15, 12.4.1 *)
Body  "[[G⊢Norm s0 −init D→ s1; G⊢s1 −c→ s2; G⊢s2 −e-≻v→ s3]] ⟹
                              G⊢Norm s0 −Body D c e-≻v→ s3"

(* evaluation of variables *)
(* cf. 15.13.1, 15.7.2 *)
LVar  "G⊢Norm s −LVar vn=≻lvar vn s→ Norm s"
(* cf. 15.10.1, 12.4.1 *)
FVar  "[[G⊢Norm s0 −init C→ s1; G⊢s1 −e-≻a→ s2;
        (v,s2') = fvar C stat fn a s2]] ⟹
        G⊢Norm s0 −{C,stat}e..fn=≻v→ s2'"
(* cf. 15.12.1, 15.25.1 *)
AVar  "[[G⊢ Norm s0 −e1-≻a→ s1; G⊢s1 −e2-≻i→ s2;
        (v,s2') = avar G i a s2]] ⟹
                    G⊢Norm s0 −e1.[e2]=≻v→ s2'"

(* evaluation of expression lists *)
(* cf. 15.11.4.2 *)
Nil
                                  "G⊢Norm s0 −[]≐≻[]→ Norm s0"

  (* cf. 15.6.4 *)
  Cons  "[[G⊢Norm s0 −e -≻ v → s1;
          G⊢  s1 −es≐≻vs→ s2]] ⟹
                                   G⊢Norm s0 −e#es≐≻v#vs→ s2"
monos
  if_def2
end

13 Evaln

(*  Title:      isabelle/Bali/Evaln.thy
    ID:         $Id: Evaln.thy,v 1.30 2000/09/08 16:37:43 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
Operational evaluation (big-step) semantics of Java expressions and statements
Variant of eval relation with counter for bounded recursive depth
Evaln could completely replace Eval.
*)
Evaln = Eval +
consts
  evaln :: "prog ⇒ (state × term × nat × vals × state) set"
syntax
  evaln :: "[prog, state, term,        nat, vals * state] => bool"
                                ("_|-_-_>-_-> _"   [61,61,80,   61,61]
60)
  evarn :: "[prog, state, var  , vvar        , nat, state] => bool"
                                ("_|-_-_=>_-_-> _" [61,61,90,61,61,61]
60)
  eval_n:: "[prog, state, expr , val         , nat, state] => bool"
                                ("_|-_-_->_-_-> _" [61,61,80,61,61,61]
60)
  evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
                                ("_|-_-_#>_-_-> _" [61,61,61,61,61,61]
60)
  execn :: "[prog, state, stmt ,               nat, state] => bool"

                              ("_|-_-_-_-> _"    [61,61,65,   61,61]
60)
syntax (xsymbols)
evaln :: "[prog, state, term,         nat, vals × state] ⇒ bool"
                              ("_⊢_−_≻−_→ _"   [61,61,80,   61,61]
60)
evarn :: "[prog, state, var  , vvar         , nat, state] ⇒ bool"
                              ("_⊢_−_=≻_−_→ _" [61,61,90,61,61,61]
60)
eval_n:: "[prog, state, expr , val ,          nat, state] ⇒ bool"
                              ("_⊢_−_-≻_−_→ _" [61,61,80,61,61,61]
60)
evalsn:: "[prog, state, expr list, val  list, nat, state] ⇒ bool"
                              ("_⊢_−_≐≻_−_→ _" [61,61,61,61,61,61]
60)
execn :: "[prog, state, stmt ,                nat, state] ⇒ bool"
                              ("_⊢_−_−_→ _"    [61,61,65,   61,61]
60)
translations
"G⊢s −e-≻v −n→ (x,s')" <= "G⊢s −In1l e≻−n→ (In1 v ,_args x s')"
"G⊢s −e-≻v −n→  s' " == "G⊢s −In1l e≻−n→ (In1 v ,        s')"
"G⊢s −e=≻vf −n→ (x,s')" <= "G⊢s −In2 e≻−n→ (In2 vf,_args x s')"
"G⊢s −e=≻vf −n→  s' " == "G⊢s −In2 e≻−n→ (In2 vf,        s')"
"G⊢s −e≐≻v −n→ (x,s')" <= "G⊢s −In3 e≻−n→ (In3 v ,_args x s')"
"G⊢s −e≐≻v −n→  s' " == "G⊢s −In3 e≻−n→ (In3 v ,        s')"
"G⊢s −c  −n→ (x,s')" <= "G⊢s −In1r c≻−n→ (In1 Unit,_args x
s')"
"G⊢s −c  −n→  s' " == "G⊢s −In1r c≻−n→ (In1 Unit,        s')"
"G⊢s −t  ≻−n→ (w,s')" <= "(s,t,n,(_args w s')) ∈ evaln G"
"G⊢s −t  ≻−n→ ws' " == "(s,t,n,        ws' ) ∈ evaln G"

inductive "evaln G" intrs
(* propagation of exceptions *)
Xcpt  "G⊢(Some xc,s) −t≻−n→ (arbitrary3 t,(Some xc,s))"

(* evaluation of variables *)

LVar  "G⊢Norm s −LVar vn=≻lvar vn s−n→ Norm s"
FVar  "[[G⊢Norm s0 −init C−n→ s1; G⊢s1 −e-≻a'−n→ s2;
        (v,s2') = fvar C stat fn a' s2]] ⟹
        G⊢Norm s0 −{C,stat}e..fn=≻v−n→ s2'"
AVar  "[[G⊢ Norm s0 −e1-≻a−n→ s1 ; G⊢s1 −e2-≻i−n→ s2;
        (v,s2') = avar G i a s2]] ⟹
                    G⊢Norm s0 −e1.[e2]=≻v−n→ s2'"

(* evaluation of expressions *)
NewC  "[[G⊢Norm s0 −init C−n→ s1;
        G⊢  s1 −halloc (CInst C)≻a→ s2]] ⟹
                                G⊢Norm s0 −NewC C-≻Addr a−n→ s2"
NewA  "[[G⊢Norm s0 −init_comp_ty T−n→ s1; G⊢s1 −e-≻i'−n→ s2;
        G⊢xupd (check_neg i') s2 −halloc (Arr T (the_Intg i'))≻a→

s3]] ⟹

                              G⊢Norm s0 −New T[e]-≻Addr a−n→ s3"
Cast  "[[G⊢Norm s0 −e-≻v−n→ s1;
        s2 = xupd (raise_if (¬G,snd s1⊢v fits T) ClassCast) s1]] ⟹
                              G⊢Norm s0 −Cast T e-≻v−n→ s2"
Inst  "[[G⊢Norm s0 −e-≻v−n→ s1;
        b = (v≠Null ∧ G,snd s1⊢v fits RefT T)]] ⟹
                            G⊢Norm s0 −e InstOf T-≻Bool b−n→ s1"
Lit                      "G⊢Norm s −Lit v-≻v−n→ Norm s"
Super                    "G⊢Norm s −Super-≻val_this s−n→ Norm s"
Acc   "[[G⊢Norm s0 −va=≻(v,f)−n→ s1]] ⟹
                                G⊢Norm s0 −Acc va-≻v−n→ s1"
Ass   "[[G⊢Norm s0 −va=≻(w,f)−n→ s1;
        G⊢  s1 −e-≻v  −n→ s2]] ⟹
                                 G⊢Norm s0 −va:=e-≻v−n→ assign f
v s2"

Cond  "[[G⊢Norm s0 −e0-≻b−n→ s1;
        G⊢  s1 −(if the_Bool b then e1 else e2)-≻v−n→ s2]] ⟹
                          G⊢Norm s0 −e0 ? e1 : e2-≻v−n→ s2"
Call  "[[G⊢Norm s0 −e-≻a'−n→ s1; G⊢s1 −args≐≻vs−n→ s2;
        C = target mode (snd s2) a' cT;
        G⊢init_lvars G C (mn,pTs) mode a' vs s2 −Methd C (mn,pTs)-≻v−n→
s3]]
    ⟹ G⊢Norm s0 −{t,cT,mode}e..mn({pTs}args)-≻v−n→ (restore_lvars
s2 s3)"
Methd "[[G⊢Norm s0 −body G C sig-≻v−n→ s1]] ⟹
                              G⊢Norm s0 −Methd C sig-≻v−Suc n→ s1"
Body  "[[G⊢Norm s0−init D−n→ s1; G⊢s1 −c−n→ s2; G⊢s2 −e-≻v−n→

s3]]⟹

                              G⊢Norm s0 −Body D c e-≻v−n→ s3"
(* evaluation of expression lists *)
Nil
                              "G⊢Norm s0 −[]≐≻[]−n→ Norm s0"
Cons  "[[G⊢Norm s0 −e -≻ v −n→ s1;
        G⊢  s1 −es≐≻vs−n→ s2]] ⟹
                           G⊢Norm s0 −e#es≐≻v#vs−n→ s2"

(* execution of statements *)
Skip                              "G⊢Norm s −Skip−n→ Norm s"
Expr  "[[G⊢Norm s0 −e-≻v−n→ s1]] ⟹
                                G⊢Norm s0 −Expr e−n→ s1"
Comp  "[[G⊢Norm s0 −c1 −n→ s1;
        G⊢  s1 −c2 −n→ s2]] ⟹
                               G⊢Norm s0 −c1;; c2−n→ s2"
If    "[[G⊢Norm s0 −e-≻b−n→ s1;
        G⊢  s1−(if the_Bool b then c1 else c2)−n→ s2]] ⟹
                     G⊢Norm s0 −If(e) c1 Else c2 −n→ s2"

  Loop  "[[G⊢Norm s0 −e-≻b−n→ s1;
          if the_Bool b then (G⊢s1 −c−n→ s2 ∧ G⊢s2 −While(e) c−n→
s3)
                        else s3 = s1]] ⟹
                              G⊢Norm s0 −While(e) c−n→ s3"
  Throw "[[G⊢Norm s0 −e-≻a'−n→ s1]] ⟹
                                 G⊢Norm s0 −Throw e−n→ xupd (throw
a') s1"
  Try   "[[G⊢Norm s0 −c1−n→ s1; G⊢s1 −sxalloc→ s2;
          if G,s2⊢catch tn then G⊢new_xcpt_var vn s2 −c2−n→ s3 else
s3 = s2]]⟹
                  G⊢Norm s0 −Try c1 Catch(tn vn) c2−n→ s3"
  Fin   "[[G⊢Norm s0 −c1−n→ (x1,s1);
          G⊢Norm s1 −c2−n→ s2]] ⟹
                   G⊢Norm s0 −c1 Finally c2−n→ xupd (xcpt_if (x1≠None)
x1) s2"
  Init  "[[the (class G C) = (sc,si,fs,ms,ini);
          if inited C (globs s0) then s3 = Norm s0
          else (G⊢Norm (init_class_obj G C s0)
                  −(if C = Object then Skip else init sc)−n→ s1 ∧
                G⊢set_lvars empty s1 −ini−n→ s2 ∧ s3 = restore_lvars
s1 s2)]]⟹
                 G⊢Norm s0 −init C−n→ s3"
monos
  if_def2
end

14 Example

(*  Title:      isabelle/Bali/Example.thy
    ID:         $Id: Example.thy,v 1.30 2000/08/07 21:07:48 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
The following example Bali 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 z) {return z;}
}
class Ext extends Base{
  int vee;
  Ext foo(Base z) {((Ext)z).vee=1; return null;}
}
class Example {
  public static void main (String args[]) {
    Base e=new Ext();
    try {e.foo(null); }
    catch (NullPointerException z) {throw z;}
  }
}
*)
Example = Eval + WellForm +
datatype tnam_= Base_| Ext_
datatype enam_= vee_| z_| e_
consts
  tnam_:: "tnam_⇒ tnam"
  enam_:: "enam_⇒ ename"
rules (* tnam_and enam_are intended to be isomorphic to tnam and ename
*)
  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"

defs
Object_mdecls_def "Object_mdecls == []"
SXcpt_mdecls_def  "SXcpt_mdecls  == []"
syntax
Base, Ext :: tname
vee, z, e :: ename
translations
"Base" == "TName (tnam_Base_)"
"Ext"  == "TName (tnam_Ext_)"
"vee"  ==        "enam_vee_"
"z"    ==        "enam_z_"
"e"    ==        "enam_e_"

consts
"classes"          :: cdecl list
BaseCl, ExtCl     :: class
Base_foo, Ext_foo :: mdecl
test              :: stmt
foo               :: mname
a,b               :: loc
defs
Base_foo_def "Base_foo ≡ ((foo,[Class Base]),
                          (False,[z],Class Base),([],Skip,!!z))"
BaseCl_def "BaseCl ≡ (Object, [],
                      [(vee, (False, PrimT Boolean))],
                      [Base_foo],
                      Skip)"
Ext_foo_def  "Ext_foo ≡ ((foo,[Class Base]),
                         (False,[z],Class Ext),
                         ([],Expr({Ext,False}Cast (Class Ext) (!!z)..
                                             vee:=Lit (Intg #1)),
                         Lit Null))"
ExtCl_def  "ExtCl ≡ (Base  , [],

                      [(vee, (False,PrimT Integer))],
                      [Ext_foo],
                      Skip)"
classes_def "classes ≡ [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
test_def "test ≡ Expr(e:==NewC Ext);;
                  Try Expr({ClassT Base,ClassT Base,IntVir}!!e..
                          foo({[Class Base]}[Lit Null]))
                  Catch((SXcpt NullPointer) z) (Throw (!!z))"
syntax
NP                         :: xname
tprg                       :: prog
obj1, obj2                 :: obj
stats,globs1,globs2        :: globs
locs1, locs2               :: locals
s0',s0,s1,s2,s3,s4,s5,s6,s7:: state
translations
"NP"      == "NullPointer"
"tprg"    == "([],classes)"
"obj1"    <= "(CInst Ext,(empty((vee, Base)↦Bool False)
                               ((vee, Ext )↦Intg #0))   (+) empty)"
"obj2"    == "(CInst(SXcpt NP),empty)"
"stats"   == "empty(Inr Ext ↦(arbitrary, empty))
                   (Inr Base ↦(arbitrary, empty))
                   (Inr Object↦(arbitrary, empty))"
"globs1"   == "stats (Inl a↦obj1)"
"globs2"   == "globs1(Inl b↦obj2)"
"locs1"    == "empty(Inr()↦Addr a)(Inl z↦Null)"
"locs2"    == "empty(Inl e↦Addr a)(Inl z↦Addr b)"
"s0'"== " Norm              (st empty  empty)"
"s0" == " Norm              (st stats  empty)"
"s1" == " Norm              (st globs1 (empty(Inl e↦Addr a)))"
"s2" == " Norm              (st globs1 locs1)"
"s3" == "(Some (StdXcpt NP), st globs1 locs1)"
"s4" == "(Some (StdXcpt NP), st globs1 (empty(Inl e↦Addr a)))"
"s5" == "(Some (XcptLoc b ), st globs2 (empty(Inl e↦Addr a)))"
"s6" == " Norm              (st globs2 locs2)"
"s7" == "(Some (XcptLoc b ), st globs2 locs2)"

end

15 Conform

(*  Title:      isabelle/Bali/Conform.thy
    ID:         $Id: Conform.thy,v 1.4 2000/09/04 16:58:05 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
Conformance notions for the type soundness proof for Java
design issues:
* lconf allows for (arbitrary) inaccessible values
* "conforms" does not directly imply that the dynamic types of all objects
on
  the heap are indeed existing classes. Yet this can be inferred for all
  referenced objs.
*)
Conform = State +
types   env_= "prog × (lname, ty) table" (* same as env of WellType.thy
*)
constdefs
  gext    :: "st ⇒ st ⇒ bool"              ("_≤|_"     [61,61]   60)
   "s≤|s' ≡ (∀ r. ∀ (oi, fs)∈globs s r: ∃ (oi',fs')∈globs s' r: oi' =
oi)"
  conf  :: "prog ⇒ st ⇒ val ⇒ ty ⇒ bool"    ("_,_⊢_::⪯_"   [61,61,61,61]
60)
           "G,s⊢v::⪯T ≡ ∃ T'∈typeof (λa. option_map obj_ty (heap s a))
v:G⊢T'⪯T"
  lconf :: "prog ⇒ st ⇒ ('a, val) table ⇒ ('a, ty) table ⇒ bool"
                                                ("_,_⊢_[::⪯]_"[61,61,61,61]
60)

           "G,s⊢vs[::⪯]Ts ≡ ∀ n. ∀ T∈Ts n: ∃ v∈vs n: G,s⊢v::⪯T"

  oconf :: "prog ⇒ st ⇒ obj ⇒ oref ⇒ bool"  ("_,_⊢_::⪯√_"  [61,61,61,61]
60)
           "G,s⊢obj::⪯√r ≡ G,s⊢snd obj[::⪯]var_tys G (fst obj) r ∧ (case
r of
                              Heap a ⇒ is_type G (obj_ty obj) | Stat
C ⇒ True)"
  conforms :: "state ⇒ env_⇒ bool"          (    "_::⪯_"   [61,61]
60)
              "xs::⪯E ≡ let (G, L) = E; s = snd xs; l = locals s in
          (∀ r. ∀ obj∈globs s r:           G,s⊢obj ::⪯√r) ∧
                                          G,s⊢l    [::⪯]L ∧
          (∀ a. fst xs=Some(XcptLoc a) ⟶ G,s⊢Addr a::⪯Class (SXcpt Throwable))"
constdefs
  DynT_prop :: "[prog,inv_mode,tname,ref_ty] ⇒ bool" ("_⊢_→_⪯_" [61,0,0,0]
61)
 "G⊢mode→D⪯t ≡ mode = IntVir ⟶ is_class G D ∧
                     (if (∃ T. t=ArrayT T) then D=Object else G⊢Class
D⪯RefT t)"
end

16 TypeSafe

(*  Title:      isabelle/Bali/TypeSafe.thy
    ID:         $Id: TypeSafe.thy,v 1.19 2000/06/26 08:52:28 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
The type soundness proof for Java
*)
TypeSafe = Eval + WellForm + Conform

17 AxSem

(*  Title:      isabelle/Bali/AxSem.thy
    ID:         $Id: AxSem.thy,v 1.101 2000/09/04 16:58:04 oheimb Exp

Axiomatic semantics of Java expressions and statements (see also Eval.thy)
design issues:
* a strong version of validity for triples with premises, namely one that
takes
  the recursive depth needed to complete execution, enables correctness
proof
* auxiliary variables are handled first-class (-> Thomas Kleymann)
* expressions not flattened to elementary assignments (as usual for axiomatic
  semantics) but treated first-class => explicit result value handling
* intermediate values not on triple, but on assertion level (with result
stack)
* because of dynamic method binding, term need to be dependent on state.
  this is also useful for conditional expressions and statements
* result values in triples exactly as in eval relation (also for xcpt
states)
* validity: additional assumption of state conformance and well-typedness,
  which is required for soundness and thus rule hazard required of completeness
restrictions:
* the rule of consequence could be polymorphic i.e. different types for
P and P'
  but the inductive definition scheme cannot handle this
*)
AxSem = Evaln + TypeSafe +
datatype  res (* result stack entry *)
          = Res   vals
          | Xcpt  xopt
          | Lcls  locals
          | DynT  tname
syntax
  Val  :: "val  ⇒ res"
  Var  :: "var  ⇒ res"
  Vals :: "val list ⇒ res"
translations
  "Val  x"     == "Res (In1 x)"

"Var  x"     == "Res (In2 x)"
"Vals x"     == "Res (In3 x)"
constdefs
the_Res  :: "res ⇒ vals"
"the_Res  y ≡ εx. y = Res x"
the_Xcpt :: "res ⇒ xopt"
"the_Xcpt y ≡ εx. y = Xcpt x"
the_Lcls :: "res ⇒ (lname, val) table"
"the_Lcls y ≡ εl. y = Lcls l"
res :: "term ⇒ vals ⇒ res list ⇒ res list"
"res t v Y ≡ if is_stmt t then Y else Res v#Y"
syntax
"Val_"    :: [pttrn] => pttrn     ("Val:_"  [951] 950)
"Var_"    :: [pttrn] => pttrn     ("Var:_"  [951] 950)
"Vals_"   :: [pttrn] => pttrn     ("Vals:_" [951] 950)
"Xcpt_"   :: [pttrn] => pttrn     ("Xcpt:_" [951] 950)
"Lcls_"   :: [pttrn] => pttrn     ("Lcls:_" [951] 950)
translations
"λVal:v . b"  == "(λv. b) ∘ (the_In1 ∘ the_Res)"
"λVar:v . b"  == "(λv. b) ∘ (the_In2 ∘ the_Res)"
"λVals:v. b"  == "(λv. b) ∘ (the_In3 ∘ the_Res)"
"λXcpt:x. b"  == "(λx. b) ∘ the_Xcpt"
"λLcls:l. b"  == "(λl. b) ∘ the_Lcls"
(* relation on result values, state and auxiliary variables *)
types rstate    =        "res list × state"
    'a assn   =        "rstate ⇒ 'a ⇒ bool"
translations
    "res"    <= (type) "AxSem.res"
    "rstate" <= (type) "res list × state"
    "a assn" <= (type) "rstate ⇒ a ⇒ bool"
constdefs
assn_imp   :: "'a assn ⇒ 'a assn ⇒ bool"             (infixr "⇒"
25)
"P ⇒ Q ≡ ∀ Y s Z. P (Y,s) Z ⟶ Q (Y,s) Z"
peek_and   :: "'a assn ⇒ (state ⇒ bool) ⇒ 'a assn" (infixl "∧."
13)
"P ∧. p ≡ λ(Y,s) Z. P (Y,s) Z ∧ p s"

assn_supd  :: "'a assn ⇒ (state ⇒ state) ⇒ 'a assn" (infixl ";."
13)
"P ;. f ≡ λ(Y,s') Z. ∃ s. P (Y,s) Z ∧ s' = f s"
supd_assn  :: "(state ⇒ state) ⇒ 'a assn ⇒ 'a assn" (infixr ".;"
13)
"f .; P ≡ λ(Y,s). P (Y,f s)"
res_push   :: "'a assn ⇒ res ⇒ 'a assn"              ("_↑#_"  [60,61]
60)
"P↑#w ≡ λ(Y,s). P (w#Y,s)"
res_eqpop :: "'a assn ⇒ res ⇒ 'a assn"               ("_↓#_"  [60,61]
60)
"P↓#w ≡ λ(Y,s) Z. ∃ Y'. Y=w#Y' ∧ P (Y',s) Z"
res_pop    :: "(res ⇒ 'a assn) ⇒ 'a assn"
"res_pop Pf ≡ λ(w#Y,s). Pf w (Y,s)"
peek_st    :: "(st ⇒ 'a assn) ⇒ 'a assn"
"peek_st Pf ≡ λ(Y,s). Pf (snd s) (Y,s)"
syntax
Normal     :: "'a assn ⇒ 'a assn"
"@res_pop"   :: "pttrn ⇒ 'a assn ⇒ 'a assn"            ("λ_#. _" [0,3]
3)
"@peek_st"   :: "pttrn ⇒ 'a assn ⇒ 'a assn"            ("λ_: _" [0,3]
3)
translations
"Normal P"  == "P ∧. normal"
"λw#ws#. P" == "res_pop (λw. λws#. P)"
"λw#.    P" == "res_pop (λw.       P)"
"λs:     P" == "peek_st (λs. P)"
constdefs
res_ign    ::  "       'a assn ⇒ 'a assn"             ("_↓" [1000]
1000)
"P↓ ≡ λw#. P"
Bool_assn  :: "'a assn ⇒ bool ⇒ 'a assn"         ("_↑#Bool=_"[60,61]
60)
"P↑#Bool=b ≡λ(Y,s) Z. ∃ v. (P↑#Val v) (Y,s) Z ∧ (normal s ⟶ the_Bool
v=b)"

constdefs
  RefVar     :: "(val ⇒ state ⇒ vvar × state) ⇒ 'a assn ⇒ 'a assn"
 "RefVar vf P ≡ λ(Val:a#Y,s). let (v,s') = vf a s in (P↑#Var v) (Y,s')"
  Alloc      :: "prog ⇒ obj_tag ⇒ 'a assn ⇒ 'a assn"
 "Alloc G otag P ≡ λ(Y,s) Z.
          ∀ s' a. G⊢s −halloc otag≻a→ s'⟶ (P↑#Val (Addr a)) (Y,s')
Z"
  SXAlloc     :: "prog ⇒ 'a assn ⇒ 'a assn"
 "SXAlloc G P ≡ λ(Y,s) Z. ∀ s'. G⊢s −sxalloc→ s' ⟶ P (Y,s') Z"
  type_ok  :: "prog ⇒ term ⇒ state ⇒ bool"
 "type_ok G t s ≡ ∃ L T. (normal s ⟶ (G,L)⊢t::T) ∧ s::⪯(G,L)"
datatype 'a triple = triple ('a assn) term ('a assn)
                                        ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
types 'a triples = 'a triple set
syntax
  var_triple   :: "['a assn, var         ,'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ _=>/ {(1_)}"    [3,80,3]
75)
  expr_triple  :: "['a assn, expr        ,'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ _->/ {(1_)}"    [3,80,3]
75)
  exprs_triple :: "['a assn, expr list   ,'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ _#>/ {(1_)}"    [3,65,3]
75)
  stmt_triple  :: "['a assn, stmt,        'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ ._./ {(1_)}"     [3,65,3]
75)
syntax (xsymbols)
  triple       :: "['a assn, term        ,'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ _≻/ {(1_)}"     [3,65,3]
75)
  var_triple   :: "['a assn, var         ,'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ _=≻/ {(1_)}"    [3,80,3]
75)
  expr_triple  :: "['a assn, expr        ,'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ _-≻/ {(1_)}"    [3,80,3]

  exprs_triple :: "['a assn, expr list   ,'a assn] ⇒ 'a triple"
                                         ("{(1_)}/ _≐≻/ {(1_)}"    [3,65,3]
75)
translations
  "{P} e-≻ {Q}" == "{P} In1l e≻ {Q}"
  "{P} e=≻ {Q}" == "{P} In2  e≻ {Q}"
  "{P} e≐≻ {Q}" == "{P} In3  e≻ {Q}"
  "{P} .c. {Q}" == "{P} In1r c≻ {Q}"
constdefs
  mtriples  :: "('c⇒ 'sig⇒ 'a assn) ⇒ ('c⇒ 'sig⇒ expr) ⇒
                ('c⇒ 'sig⇒ 'a assn) ⇒ ('c × 'sig)set ⇒ 'a triples"
                                     ("{{(1_)}/ _-≻/ {(1_)} | _}"[3,65,3,65]75)
 "{{P} mb-≻ {Q} | ms} ≡ (λ(C,sig). {Normal(P C sig)} mb C sig-≻ {Q C
sig})``ms"
consts
 triple_valid :: "prog ⇒ nat ⇒  'a triple ⇒ bool"
                                                (   "_⊧_:_" [61,0, 58]
57)
    ax_valids :: "prog ⇒ 'a triples ⇒ 'a triples ⇒ bool"
                                                ("_,_|⊧_"   [61,58,58]
57)
    ax_derivs :: "prog ⇒ ('a triples × 'a triples) set"
syntax
 triples_valid:: "prog ⇒ nat ⇒  'a triples ⇒ bool"
                                                (  "_||=_:_" [61,0, 58]
57)
     ax_valid :: "prog ⇒ 'a triples ⇒ 'a triple ⇒ bool"
                                                ( "_,_|=_"   [61,58,58]
57)
     ax_Derivs:: "prog ⇒ 'a triples ⇒ 'a triples ⇒ bool"
                                                ("_,_||-_"   [61,58,58]
57)
     ax_Deriv :: "prog ⇒ 'a triples ⇒ 'a triple ⇒ bool"
                                                ( "_,_|-_"   [61,58,58]
57)
syntax (xsymbols)

 triples_valid:: "prog ⇒ nat ⇒  'a triples ⇒ bool"
                                                (  "_|⊧_:_" [61,0, 58]
57)
     ax_valid :: "prog ⇒ 'a triples ⇒ 'a triple ⇒ bool"
                                                ( "_,_⊧_"   [61,58,58]
57)
     ax_Derivs:: "prog ⇒ 'a triples ⇒ 'a triples ⇒ bool"
                                                ("_,_|⊢_"   [61,58,58]
57)
     ax_Deriv :: "prog ⇒ 'a triples ⇒ 'a triple ⇒ bool"
                                                ( "_,_⊢_"   [61,58,58]
57)
defs  triple_valid_def   "G⊧n:t ≡ case t of {P} t≻ {Q} ⇒
                          ∀ Y s Z. P (Y,s) Z ⟶ type_ok G t s ⟶
                          (∀ w s'. G⊢s −t≻−n→ (w,s') ⟶ Q (res t w
Y,s') Z)"
translations        "G|⊧n:ts"  == "Ball ts (triple_valid G n)"
defs     ax_valids_def "G,A|⊧ts ≡ ∀ n. G|⊧n:A ⟶ G|⊧n:ts"
translations         "G,A ⊧t"   == "G,A|⊧{t}"
                     "G,A|⊢ts"  == "(A,ts) ∈ ax_derivs G"
                     "G,A ⊢t"   == "G,A|⊢{t}"
inductive "ax_derivs G" intrs
  empty " G,A|⊢{}"
  insert"[[G,A⊢t; G,A|⊢ts]] ⟹
          G,A|⊢insert t ts"
  asm    "ts⊆A ⟹ G,A|⊢ts"
(* could be added for convenience and efficiency, but is not necessary
  cut    "[[G,A'|⊢ts; G,A|⊢A']] ⟹
           G,A |⊢ts"
*)
  weaken"[[G,A|⊢ts'; ts ⊆ ts']] ⟹ G,A|⊢ts"
  conseq"∀ Y s Z . P  (Y ,s) Z ⟶ (∃ P' Q'. G,A⊢{P'} t≻ {Q'} ∧ (∀ w
s'.
        (∀ Y'  Z'. P' (Y',s) Z' ⟶ Q' (res t w Y',s') Z')
                               ⟶ Q  (res t w Y ,s') Z ))
                                         ⟹ G,A⊢{P } t≻ {Q }"

hazard"G,A⊢{P ∧. Not ∘ type_ok G t} t≻ {Q}"
Xcpt  "G,A⊢{(λ(Y,s). P (res t (arbitrary3 t) Y,s)) ∧. Not ∘ normal}
t≻ {P}"
(* variables *)
LVar  " G,A⊢{Normal (λs: P↑#Var (lvar vn s))} LVar vn=≻ {P}"
FVar  "[[G,A⊢{Normal P} .init C. {Q};
        G,A⊢{Q} e-≻ {RefVar (fvar C stat fn) R}]] ⟹
                                G,A⊢{Normal P} {C,stat}e..fn=≻ {R}"
AVar  "[[G,A⊢{Normal P} e1-≻ {Q};
        G,A⊢{Q} e2-≻ {λVal:i#. RefVar (avar G i) R}]] ⟹
                                 G,A⊢{Normal P} e1.[e2]=≻ {R}"
(* expressions *)
NewC  "[[G,A⊢{Normal P} .init C. {Alloc G (CInst C) Q}]] ⟹
                                        G,A⊢{Normal P} NewC C-≻ {Q}"
NewA  "[[G,A⊢{Normal P} .init_comp_ty T. {Q};
        G,A⊢{Q} e-≻ {λVal:i#. xupd (check_neg i) .; Alloc G (Arr T
(the_Intg i)) R}]]
       ⟹  G,A⊢{Normal P} New T[e]-≻ {R}"
Cast  "[[G,A⊢{Normal P} e-≻ {λVal:v#. λs:
        xupd (raise_if (¬G,s⊢v fits T) ClassCast) .; Q↑#Val v}]] ⟹
                               G,A⊢{Normal P} Cast T e-≻ {Q}"
Inst  "[[G,A⊢{Normal P} e-≻ {λVal:v#. λs:
                Q↑#Val (Bool (v≠Null ∧ G,s⊢v fits RefT T))}]] ⟹
                               G,A⊢{Normal P} e InstOf T-≻ {Q}"
Lit                           "G,A⊢{Normal (P↑#Val v)} Lit v-≻ {P}"
Super " G,A⊢{Normal (λs: P↑#Val (val_this s))} Super-≻ {P}"
Acc   "[[G,A⊢{Normal P} va=≻ {λVar:(v,f)#. Q↑#Val v}]] ⟹
                               G,A⊢{Normal P} Acc va-≻ {Q}"
Ass   "[[G,A⊢{Normal P} va=≻ {Q};
        G,A⊢{Q} e-≻ {λVal:v#Var:(w,f)#. assign f v .; R↑#Val v}]] ⟹
                               G,A⊢{Normal P} va:=e-≻ {R}"

Cond  "[[G,A ⊢{Normal P} e0-≻ {P'};
        ∀ b. G,A⊢{P'↑#Bool=b} (if b then e1 else e2)-≻ {Q}]]
                            ⟹ G,A⊢{Normal P} e0 ? e1 : e2-≻ {Q}"
Call  "[[G,A⊢{Normal P} e-≻ {Q};
        G,A⊢{Q} args≐≻ {λVals:vs#Val:a#. λs: let D=target mode s a
cT
    in (init_lvars G D (mn,pTs) mode a vs .; R↑#DynT D↑#Lcls (locals
s))};
     ∀ D. G,A⊢{R↑#DynT D∧.(λs. normal s ⟶ G⊢mode→D⪯t)} Methd D
(mn,pTs)-≻
               {λVal:v#Lcls:l#. set_lvars l .; S↑#Val v}]]⟹
       G,A⊢{Normal P} {t,cT,mode}e..mn({pTs}args)-≻ {S}"
Methd "[[G,A∪ {{P} Methd-≻ {Q} | ms} |⊢ {{P} body G-≻ {Q} | ms}]] ⟹
                                   G,A|⊢{{P} Methd-≻ {Q} | ms}"
Body  "[[G,A⊢{Normal P} .init D. {Q}; G,A⊢{Q} .c. {R}; G,A⊢{R} e-≻
{S}]] ⟹
                               G,A⊢{Normal P} Body D c e-≻ {S}"
(* expression lists *)
Nil                           "G,A⊢{Normal (P↑#Vals [])} []≐≻ {P}"
Cons  "[[G,A⊢{Normal P} e-≻ {Q};
        G,A⊢{Q} es≐≻ {λVals:vs#Val:v#. R↑#Vals (v#vs)}]] ⟹
                               G,A⊢{Normal P} e#es≐≻ {R}"
(* statements *)
Skip                          "G,A⊢{Normal P} .Skip. {P}"
Expr  "[[G,A⊢{Normal P} e-≻ {Q↓}]] ⟹
                               G,A⊢{Normal P} .Expr e. {Q}"
Comp  "[[G,A⊢{Normal P} .c1. {Q};
        G,A⊢{Q} .c2. {R}]] ⟹
                               G,A⊢{Normal P} .c1;;c2. {R}"
If    "[[G,A ⊢{Normal P} e-≻ {P'};
        ∀ b. G,A⊢{P'↑#Bool=b} .(if b then c1 else c2). {Q}]] ⟹
                     G,A⊢{Normal P} .If(e) c1 Else c2. {Q}"
(* unfolding variant of Loop, not needed here

  LoopU "[[G,A ⊢{Normal P} e-≻ {P'};
          ∀ b. G,A⊢{P'↑#Bool=b} .(if b then c;;While(e) c else Skip).{Q}]]
         ⟹  G,A⊢{Normal P} .While(e) c. {Q}"
*)
  Loop  "[[G,A⊢{P} e-≻ {P'}; G,A⊢{P'↑#Bool=True} .c. {P}]] ⟹
                  G,A⊢{P} .While(e) c. {P'↑#Bool=False}"
  Throw "[[G,A⊢{Normal P} e-≻ {λVal:a#. xupd (throw a) .; Q}]] ⟹
          G,A⊢{Normal P} .Throw e. {Q}"
  Try   "[[G,A⊢{Normal P} .c1. {SXAlloc G Q};
          G,A⊢{Q ∧. (λs.  G,s⊢catch C) ;. new_xcpt_var vn} .c2. {R};
          (Q ∧. (λs. ¬G,s⊢catch C)) ⇒ R]] ⟹
                 G,A⊢{Normal P} .Try c1 Catch(C vn) c2. {R}"
  Fin   "[[G,A⊢{Normal P}.c1.{λ(Y,(x,s)). (Q↑#Xcpt x) (Y,Norm s)};
          G,A⊢{Normal Q}.c2.{λXcpt:x'#. xupd (xcpt_if (x'≠None) x') .;
R}]]
         ⟹  G,A⊢{Normal P} .c1 Finally c2. {R}"
  Done  " G,A⊢{Normal (P ∧. initd C)} .init C. {P}"
  Init  "[[the (class G C) = (sc,si,fs,ms,ini);
          G,A⊢{Normal ((P ∧. Not ∘ initd C) ;. supd (init_class_obj G
C))}
              .(if C = Object then Skip else init sc).
              {λs: Q↑#Lcls (locals s)};
          G,A⊢{Q ;. set_lvars empty} .ini. {λLcls:l#. set_lvars l .; R}]]
         ⟹ G,A⊢{Normal (P ∧. Not ∘ initd C)} .init C. {R}"
end

18 AxExample

(*  Title:      isabelle/Bali/AxExample.thy
    ID:         $Id: AxExample.thy,v 1.3 2000/03/30 09:38:10 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   2000 Technische Universitaet Muenchen
*)
AxExample = AxSem + Example

19 AxSound

(*  Title:      isabelle/Bali/AxSound.thy
    ID:         $Id: AxSound.thy,v 1.9 2000/08/07 21:07:48 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
Soundness proof for Axiomatic semantics of Java expressions and statements
*)
AxSound = AxSem +
consts
 triple_valid2:: "prog ⇒ nat ⇒  'a triple ⇒ bool"
                                                (   "_⊧_::_"[61,0, 58]
57)
    ax_valids2:: "prog ⇒ 'a triples ⇒ 'a triples ⇒ bool"
                                                ("_,_|⊧::_" [61,58,58]
57)
defs  triple_valid2_def  "G⊧n::t ≡ case t of {P} t≻ {Q} ⇒
 ∀ Y s Z. P (Y,s) Z ⟶ (∀ L. s::⪯(G,L) ⟶ (∀ T. (normal s ⟶ (G,L)⊢t::T)

⟶

               (∀ w s'. G⊢s −t≻−n→ (w,s') ⟶ Q (res t w Y,s') Z ∧
s'::⪯(G,L))))"
defs  ax_valids2_def  "G,A|⊧::ts ≡ ∀ n. (∀ t∈A. G⊧n::t) ⟶ (∀ t∈ts.
G⊧n::t)"
end

20 AxCompl

(*  Title:      isabelle/Bali/AxCompl.thy
    ID:         $Id: AxCompl.thy,v 1.30 2000/09/13 13:51:57 oheimb Exp
$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Completeness proof for Axiomatic semantics of Java expressions and statements
design issues:
* proof structured by Most General Formulas (-> Thomas Kleymann)
*)
AxCompl = AxSem +
constdefs
  nyinitcls :: "prog ⇒ state ⇒ tname set"
 "nyinitcls G s ≡ {C. is_class G C ∧ ¬ initd C s}"
  init_le :: "prog ⇒ nat ⇒ state ⇒ bool"            ("_⊢init≤_"  [51,51]
50)
 "G⊢init≤n ≡ λs. card (nyinitcls G s) ≤ n"
consts (* Most General Triples and Formulas *)
  MGF  ::"[rstate assn,term,prog]⇒rstate triple"   ("{_} _≻ {_→}"[3,65,3]62)
  MGFn ::"[nat        ,term,prog]⇒rstate triple" ("{=:_} _≻ {_→}"[3,65,3]62)
defs
  MGF_def
  "{P} t≻ {G→} ≡ {P} t≻ {λ(Y',s') (Y,s). ∃ w. Y'=res t w Y ∧ G⊢s −t≻→
(w,s')}"
  MGFn_def
  "{=:n} t≻ {G→} ≡ {op = ∧. G⊢init≤n} t≻ {G→}"
end

65