src/HOL/Bali/Eval.thy
changeset 12925 99131847fb93
parent 12919 d6a0d168291e
child 13337 f75dfc606ac7
     1.1 --- a/src/HOL/Bali/Eval.thy	Thu Feb 21 20:11:32 2002 +0100
     1.2 +++ b/src/HOL/Bali/Eval.thy	Fri Feb 22 11:26:44 2002 +0100
     1.3 @@ -370,7 +370,14 @@
     1.4  	          n = Inl (fn,C); 
     1.5                    f = (\<lambda>v. supd (upd_gobj oref n v)) 
     1.6        in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
     1.7 -
     1.8 +(*
     1.9 + "fvar C stat fn a' s 
    1.10 +    \<equiv> let (oref,xf) = if stat then (Stat C,id)
    1.11 +                              else (Heap (the_Addr a'),np a');
    1.12 +	          n = Inl (fn,C); 
    1.13 +                  f = (\<lambda>v. supd (upd_gobj oref n v)) 
    1.14 +      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
    1.15 +*)
    1.16    avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
    1.17   "avar G i' a' s 
    1.18      \<equiv> let   oref = Heap (the_Addr a'); 
    1.19 @@ -412,7 +419,32 @@
    1.20  apply (simp (no_asm) add: Let_def split_beta)
    1.21  done
    1.22  
    1.23 +constdefs
    1.24 +check_field_access::
    1.25 +"prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
    1.26 +"check_field_access G accC statDeclC fn stat a' s
    1.27 + \<equiv> let oref = if stat then Stat statDeclC
    1.28 +                      else Heap (the_Addr a');
    1.29 +       dynC = case oref of
    1.30 +                   Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
    1.31 +                 | Stat C \<Rightarrow> C;
    1.32 +       f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
    1.33 +   in abupd 
    1.34 +        (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
    1.35 +                  AccessViolation)
    1.36 +        s"
    1.37  
    1.38 +constdefs
    1.39 +check_method_access:: 
    1.40 +  "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
    1.41 +"check_method_access G accC statT mode sig  a' s
    1.42 + \<equiv> let invC = invocation_class mode (store s) a' statT;
    1.43 +       dynM = the (dynlookup G statT invC sig)
    1.44 +   in abupd 
    1.45 +        (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
    1.46 +                  AccessViolation)
    1.47 +        s"
    1.48 +       
    1.49  section "evaluation judgments"
    1.50  
    1.51  consts
    1.52 @@ -552,7 +584,27 @@
    1.53  	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
    1.54                \<Longrightarrow>
    1.55  		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
    1.56 -
    1.57 +   (* This class initialisation rule is a little bit inaccurate. Look at the
    1.58 +      exact sequence:
    1.59 +      1. The current class object (the static fields) are initialised
    1.60 +         (init_class_obj)
    1.61 +      2. Then the superclasses are initialised
    1.62 +      3. The static initialiser of the current class is invoked
    1.63 +      More precisely we should expect another ordering, namely 2 1 3.
    1.64 +      But we can't just naively toggle 1 and 2. By calling init_class_obj 
    1.65 +      before initialising the superclasses we also implicitly record that
    1.66 +      we have started to initialise the current class (by setting an 
    1.67 +      value for the class object). This becomes 
    1.68 +      crucial for the completeness proof of the axiomatic semantics 
    1.69 +      (AxCompl.thy). Static initialisation requires an induction on the number 
    1.70 +      of classes not yet initialised (or to be more precise, classes where the
    1.71 +      initialisation has not yet begun). 
    1.72 +      So we could first assign a dummy value to the class before
    1.73 +      superclass initialisation and afterwards set the correct values.
    1.74 +      But as long as we don't take memory overflow into account 
    1.75 +      when allocating class objects, and don't model definite assignment in
    1.76 +      the static initialisers, we can leave things as they are for convenience. 
    1.77 +   *)
    1.78  (* evaluation of expressions *)
    1.79  
    1.80    (* cf. 15.8.1, 12.4.1 *)
    1.81 @@ -602,10 +654,15 @@
    1.82    Call:	
    1.83    "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
    1.84      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
    1.85 -    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2 
    1.86 -         \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s3\<rbrakk>
    1.87 +    s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
    1.88 +    s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
    1.89 +    G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
    1.90     \<Longrightarrow>
    1.91 -       G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s3)"
    1.92 +       G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
    1.93 +(* The accessibility check is after init_lvars, to keep it simple. Init_lvars 
    1.94 +   already tests for the absence of a null-pointer reference in case of an
    1.95 +   instance method invocation
    1.96 +*)
    1.97  
    1.98    Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
    1.99  				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   1.100 @@ -620,9 +677,14 @@
   1.101    LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
   1.102  
   1.103    (* cf. 15.10.1, 12.4.1 *)
   1.104 -  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   1.105 -	  (v,s2') = fvar C stat fn a s2\<rbrakk> \<Longrightarrow>
   1.106 -	  G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<rightarrow> s2'"
   1.107 +  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   1.108 +	  (v,s2') = fvar statDeclC stat fn a s2;
   1.109 +          s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
   1.110 +	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
   1.111 + (* The accessibility check is after fvar, to keep it simple. Fvar already
   1.112 +    tests for the absence of a null-pointer reference in case of an instance
   1.113 +    field
   1.114 +  *)
   1.115  
   1.116    (* cf. 15.12.1, 15.25.1 *)
   1.117    AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
   1.118 @@ -688,35 +750,35 @@
   1.119  inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
   1.120  
   1.121  inductive_cases eval_elim_cases:
   1.122 -        "G\<turnstile>(Some xc,s) \<midarrow>t                         \<succ>\<rightarrow> vs'"
   1.123 -	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<rightarrow> xs'"
   1.124 -        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<rightarrow> xs'"
   1.125 -        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<rightarrow> xs'"
   1.126 -	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<rightarrow> vs'"
   1.127 -	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<rightarrow> vs'"
   1.128 -	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<rightarrow> vs'"
   1.129 -	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<rightarrow> vs'"
   1.130 -	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<rightarrow> vs'"
   1.131 -	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<rightarrow> vs'"
   1.132 -	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<rightarrow> vs'"
   1.133 -	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<rightarrow> vs'"
   1.134 -	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<rightarrow> xs'"
   1.135 -	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<rightarrow> xs'"
   1.136 -	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<rightarrow> xs'"
   1.137 -	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<rightarrow> xs'"
   1.138 -	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<rightarrow> vs'"
   1.139 -	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<rightarrow> xs'"
   1.140 -	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<rightarrow> xs'"
   1.141 -	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<rightarrow> xs'"
   1.142 -	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<rightarrow> xs'"
   1.143 -	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<rightarrow> vs'"
   1.144 -	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<rightarrow> vs'"
   1.145 -	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<rightarrow> vs'"
   1.146 -	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<rightarrow> xs'"
   1.147 -	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<rightarrow> vs'"
   1.148 -	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<rightarrow> vs'"
   1.149 -	"G\<turnstile>Norm s \<midarrow>In1l ({statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
   1.150 -	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<rightarrow> xs'"
   1.151 +        "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> vs'"
   1.152 +	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> xs'"
   1.153 +        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                         \<succ>\<rightarrow> xs'"
   1.154 +        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> xs'"
   1.155 +	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"
   1.156 +	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"
   1.157 +	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"
   1.158 +	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"
   1.159 +	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"
   1.160 +	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"
   1.161 +	"G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> vs'"
   1.162 +	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> vs'"
   1.163 +	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> xs'"
   1.164 +	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> xs'"
   1.165 +	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> xs'"
   1.166 +	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> xs'"
   1.167 +	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> vs'"
   1.168 +	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> xs'"
   1.169 +	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> xs'"
   1.170 +	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> xs'"
   1.171 +	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> xs'"
   1.172 +	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> vs'"
   1.173 +	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> vs'"
   1.174 +	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> vs'"
   1.175 +	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> xs'"
   1.176 +	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> vs'"
   1.177 +	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> vs'"
   1.178 +	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
   1.179 +	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> xs'"
   1.180  declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
   1.181  declare split_paired_All [simp] split_paired_Ex [simp]
   1.182  ML_setup {*
   1.183 @@ -851,12 +913,14 @@
   1.184  apply (case_tac "s", case_tac "a = None")
   1.185  by (auto intro!: eval.Methd)
   1.186  
   1.187 -lemma eval_Call: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
   1.188 -       D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   1.189 -       G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2 
   1.190 -        \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s3; 
   1.191 -       s3' = restore_lvars s2 s3\<rbrakk> \<Longrightarrow>  
   1.192 -       G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s3'"
   1.193 +lemma eval_Call: 
   1.194 +   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
   1.195 +     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   1.196 +     s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
   1.197 +     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   1.198 +     G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; 
   1.199 +       s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>  
   1.200 +       G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
   1.201  apply (drule eval.Call, assumption)
   1.202  apply (rule HOL.refl)
   1.203  apply simp+