src/HOL/Bali/Trans.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
schirmer@12854
     1
(*  Title:      isabelle/Bali/Trans.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
schirmer@12854
     4
    Copyright   1997 Technische Universitaet Muenchen
schirmer@12854
     5
schirmer@12854
     6
Operational transition (small-step) semantics of the 
schirmer@12854
     7
execution of Java expressions and statements
schirmer@12854
     8
schirmer@12854
     9
PRELIMINARY!!!!!!!!
schirmer@12854
    10
schirmer@12854
    11
*)
schirmer@12854
    12
schirmer@12854
    13
Trans = Eval +
schirmer@12854
    14
schirmer@12854
    15
consts
schirmer@12854
    16
  texpr_tstmt	:: "prog \<Rightarrow> (((expr \<times> state) \<times> (expr \<times> state)) +
schirmer@12854
    17
		            ((stmt \<times> state) \<times> (stmt \<times> state))) set"
schirmer@12854
    18
schirmer@12854
    19
syntax (symbols)
schirmer@12854
    20
  texpr :: "[prog, expr \<times> state, expr \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<rightarrow>1 _"[61,82,82] 81)
schirmer@12854
    21
  tstmt :: "[prog, stmt \<times> state, stmt \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
schirmer@12854
    22
  Ref   :: "loc \<Rightarrow> expr"
schirmer@12854
    23
schirmer@12854
    24
translations
schirmer@12854
    25
schirmer@12854
    26
  "G\<turnstile>e_s \<rightarrow>1 ex_s'" == "Inl (e_s, ex_s') \<in> texpr_tstmt G"
schirmer@12854
    27
  "G\<turnstile>s_s \<mapsto>1 s'_s'" == "Inr (s_s, s'_s') \<in> texpr_tstmt G"
schirmer@12854
    28
  "Ref a" == "Lit (Addr a)"
schirmer@12854
    29
schirmer@12854
    30
inductive "texpr_tstmt G" intrs 
schirmer@12854
    31
schirmer@12854
    32
(* evaluation of expression *)
schirmer@12854
    33
  (* cf. 15.5 *)
schirmer@12854
    34
  XcptE	"\<lbrakk>\<forall>v. e \<noteq> Lit v\<rbrakk> \\<Longrightarrow>
schirmer@12854
    35
				  G\<turnstile>(e,Some xc,s) \<rightarrow>1 (Lit arbitrary,Some xc,s)"
schirmer@12854
    36
schirmer@12854
    37
  (* cf. 15.8.1 *)
schirmer@12854
    38
  NewC	"\<lbrakk>new_Addr (heap s) = Some (a,x);
schirmer@12854
    39
	  s' = assign (hupd[a\<mapsto>init_Obj G C]s) (x,s)\<rbrakk> \\<Longrightarrow>
schirmer@12854
    40
				G\<turnstile>(NewC C,None,s) \<rightarrow>1 (Ref a,s')"
schirmer@12854
    41
schirmer@12854
    42
  (* cf. 15.9.1 *)
schirmer@12854
    43
  NewA1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    44
			      G\<turnstile>(New T[e],None,s) \<rightarrow>1 (New T[e'],s')"
schirmer@12854
    45
  NewA	"\<lbrakk>i = the_Intg i'; new_Addr (heap s) = Some (a, x);
schirmer@12854
    46
	  s' = assign (hupd[a\<mapsto>init_Arr T i]s)(raise_if (i<#0) NegArrSize x,s)\<rbrakk> \\<Longrightarrow>
schirmer@12854
    47
			G\<turnstile>(New T[Lit i'],None,s) \<rightarrow>1 (Ref a,s')"
schirmer@12854
    48
  (* cf. 15.15 *)
schirmer@12854
    49
  Cast1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    50
			      G\<turnstile>(Cast T e,None,s) \<rightarrow>1 (Cast T e',s')"
schirmer@12854
    51
  Cast	"\<lbrakk>x'= raise_if (\<questiondown>G,s\<turnstile>v fits T) ClassCast None\<rbrakk> \\<Longrightarrow>
schirmer@12854
    52
		        G\<turnstile>(Cast T (Lit v),None,s) \<rightarrow>1 (Lit v,x',s)"
schirmer@12854
    53
schirmer@12854
    54
  (* cf. 15.7.1 *)
schirmer@12854
    55
(*Lit				"G\<turnstile>(Lit v,None,s) \<rightarrow>1 (Lit v,None,s)"*)
schirmer@12854
    56
schirmer@12854
    57
  (* cf. 15.13.1, 15.2 *)
schirmer@12854
    58
  LAcc	"\<lbrakk>v = the (locals s vn)\<rbrakk> \\<Longrightarrow>
schirmer@12854
    59
			       G\<turnstile>(LAcc vn,None,s) \<rightarrow>1 (Lit v,None,s)"
schirmer@12854
    60
schirmer@12854
    61
  (* cf. 15.25.1 *)
schirmer@12854
    62
  LAss1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    63
				 G\<turnstile>(f vn:=e,None,s) \<rightarrow>1 (vn:=e',s')"
schirmer@12854
    64
  LAss			    "G\<turnstile>(f vn:=Lit v,None,s) \<rightarrow>1 (Lit v,None,lupd[vn\<mapsto>v]s)"
schirmer@12854
    65
schirmer@12854
    66
  (* cf. 15.10.1, 15.2 *)
schirmer@12854
    67
  FAcc1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    68
			       G\<turnstile>({T}e..fn,None,s) \<rightarrow>1 ({T}e'..fn,s')"
schirmer@12854
    69
  FAcc	"\<lbrakk>v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T))\<rbrakk> \\<Longrightarrow>
schirmer@12854
    70
			  G\<turnstile>({T}Lit a'..fn,None,s) \<rightarrow>1 (Lit v,np a' None,s)"
schirmer@12854
    71
schirmer@12854
    72
  (* cf. 15.25.1 *)
schirmer@12854
    73
  FAss1	"\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    74
			  G\<turnstile>(f ({T}e1..fn):=e2,None,s) \<rightarrow>1 (f({T}e1'..fn):=e2,s')"
schirmer@12854
    75
  FAss2	"\<lbrakk>G\<turnstile>(e2,np a' None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    76
		      G\<turnstile>(f({T}Lit a'..fn):=e2,None,s) \<rightarrow>1 (f({T}Lit a'..fn):=e2',s')"
schirmer@12854
    77
  FAss	"\<lbrakk>a = the_Addr a'; (c,fs) = the_Obj (heap s a);
schirmer@12854
    78
	  s'= assign (hupd[a\<mapsto>Obj c (fs[(fn,T)\<mapsto>v])]s) (None,s)\<rbrakk> \\<Longrightarrow>
schirmer@12854
    79
		   G\<turnstile>(f({T}Lit a'..fn):=Lit v,None,s) \<rightarrow>1 (Lit v,s')"
schirmer@12854
    80
schirmer@12854
    81
schirmer@12854
    82
schirmer@12854
    83
schirmer@12854
    84
schirmer@12854
    85
  (* cf. 15.12.1 *)
schirmer@12854
    86
  AAcc1	"\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    87
				G\<turnstile>(e1[e2],None,s) \<rightarrow>1 (e1'[e2],s')"
schirmer@12854
    88
  AAcc2	"\<lbrakk>G\<turnstile>(e2,None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    89
			    G\<turnstile>(Lit a'[e2],None,s) \<rightarrow>1 (Lit a'[e2'],s')"
schirmer@12854
    90
  AAcc	"\<lbrakk>vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
schirmer@12854
    91
	  x' = raise_if (vo = None) IndOutBound (np a' None)\<rbrakk> \\<Longrightarrow>
schirmer@12854
    92
			G\<turnstile>(Lit a'[Lit i'],None,s) \<rightarrow>1 (Lit (the vo),x',s)"
schirmer@12854
    93
schirmer@12854
    94
schirmer@12854
    95
  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
schirmer@12854
    96
  Call1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    97
			  G\<turnstile>(e..mn({pT}p),None,s) \<rightarrow>1 (e'..mn({pT}p),s')"
schirmer@12854
    98
  Call2	"\<lbrakk>G\<turnstile>(p,None,s) \<rightarrow>1 (p',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
    99
		     G\<turnstile>(Lit a'..mn({pT}p),None,s) \<rightarrow>1 (Lit a'..mn({pT}p'),s')"
schirmer@12854
   100
  Call	"\<lbrakk>a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
schirmer@12854
   101
 			   the (cmethd G (fst (the_Obj (h a))) (mn,pT))\<rbrakk> \\<Longrightarrow>
schirmer@12854
   102
	    G\<turnstile>(Lit a'..mn({pT}Lit pv),None,(h,l)) \<rightarrow>1 
schirmer@12854
   103
      (Body blk res l,np a' x,(h,init_vals lvars[This\<mapsto>a'][Super\<mapsto>a'][pn\<mapsto>pv]))"
schirmer@12854
   104
  Body1	"\<lbrakk>G\<turnstile>(s0,None,s) \<mapsto>1 (s0',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
   105
		   G\<turnstile>(Body s0    e      l,None,s) \<rightarrow>1 (Body s0'  e  l,s')"
schirmer@12854
   106
  Body2	"\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
   107
		   G\<turnstile>(Body Skip  e      l,None,s) \<rightarrow>1 (Body Skip e' l,s')"
schirmer@12854
   108
  Body		  "G\<turnstile>(Body Skip (Lit v) l,None,s) \<rightarrow>1 (Lit v,None,(heap s,l))"
schirmer@12854
   109
schirmer@12854
   110
(* execution of statements *)
schirmer@12854
   111
schirmer@12854
   112
  (* cf. 14.1 *)
schirmer@12854
   113
  XcptS	"\<lbrakk>s0 \<noteq> Skip\<rbrakk> \\<Longrightarrow>
schirmer@12854
   114
				 G\<turnstile>(s0,Some xc,s) \<mapsto>1 (Skip,Some xc,s)"
schirmer@12854
   115
schirmer@12854
   116
  (* cf. 14.5 *)
schirmer@12854
   117
(*Skip	 			 "G\<turnstile>(Skip,None,s) \<mapsto>1 (Skip,None,s)"*)
schirmer@12854
   118
schirmer@12854
   119
  (* cf. 14.2 *)
schirmer@12854
   120
  Comp1	"\<lbrakk>G\<turnstile>(s1,None,s) \<mapsto>1 (s1',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
   121
			       G\<turnstile>(s1;; s2,None,s) \<mapsto>1 (s1';; s2,s')"
schirmer@12854
   122
  Comp			    "G\<turnstile>(Skip;; s2,None,s) \<mapsto>1 (s2,None,s)"
schirmer@12854
   123
schirmer@12854
   124
schirmer@12854
   125
schirmer@12854
   126
schirmer@12854
   127
schirmer@12854
   128
schirmer@12854
   129
  (* cf. 14.7 *)
schirmer@12854
   130
  Expr1	"\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
   131
				G\<turnstile>(Expr e,None,s) \<mapsto>1 (Expr e',s')"
schirmer@12854
   132
  Expr			 "G\<turnstile>(Expr (Lit v),None,s) \<mapsto>1 (Skip,None,s)"
schirmer@12854
   133
schirmer@12854
   134
  (* cf. 14.8.2 *)
schirmer@12854
   135
  If1	"\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
schirmer@12854
   136
		      G\<turnstile>(If(e) s1 Else s2,None,s) \<mapsto>1 (If(e') s1 Else s2,s')"
schirmer@12854
   137
  If		 "G\<turnstile>(If(Lit v) s1 Else s2,None,s) \<mapsto>1 
schirmer@12854
   138
		    (if the_Bool v then s1 else s2,None,s)"
schirmer@12854
   139
schirmer@12854
   140
  (* cf. 14.10, 14.10.1 *)
schirmer@12854
   141
  Loop			  "G\<turnstile>(While(e) s0,None,s) \<mapsto>1 
schirmer@12854
   142
			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
schirmer@12854
   143
schirmer@12854
   144
end