5 |
5 |
6 Operational evaluation (big-step) semantics of the |
6 Operational evaluation (big-step) semantics of the |
7 execution of Java expressions and statements |
7 execution of Java expressions and statements |
8 *) |
8 *) |
9 |
9 |
10 Eval = State + |
10 Eval = State + WellType + |
11 |
11 |
12 consts |
12 consts |
13 eval :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set" |
13 eval :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set" |
14 evals :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set" |
14 evals :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set" |
15 exec :: "java_mb prog \\<Rightarrow> (xstate \\<times> stmt \\<times> xstate) set" |
15 exec :: "java_mb prog \\<Rightarrow> (xstate \\<times> stmt \\<times> xstate) set" |
71 (* cf. 15.25.1 *) |
71 (* cf. 15.25.1 *) |
72 FAss "\\<lbrakk>G\\<turnstile> Norm s0 -e1\\<succ>a'\\<rightarrow> (x1,s1); a = the_Addr a'; |
72 FAss "\\<lbrakk>G\\<turnstile> Norm s0 -e1\\<succ>a'\\<rightarrow> (x1,s1); a = the_Addr a'; |
73 G\\<turnstile>(np a' x1,s1) -e2\\<succ>v \\<rightarrow> (x2,s2); |
73 G\\<turnstile>(np a' x1,s1) -e2\\<succ>v \\<rightarrow> (x2,s2); |
74 h = heap s2; (c,fs) = the (h a); |
74 h = heap s2; (c,fs) = the (h a); |
75 h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))\\<rbrakk> \\<Longrightarrow> |
75 h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))\\<rbrakk> \\<Longrightarrow> |
76 G\\<turnstile>Norm s0 -{T}e1..fn\\<in>=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)" |
76 G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)" |
77 |
77 |
78 (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *) |
78 (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *) |
79 Call "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a'; |
79 Call "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a'; |
80 G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a)); |
80 G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a)); |
81 (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); |
81 (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); |