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 + WellType + |
10 Eval = State + WellType + |
11 |
|
12 consts |
11 consts |
13 eval :: "java_mb prog => (xstate \\<times> expr \\<times> val \\<times> xstate) set" |
12 eval :: "java_mb prog => (xstate \\<times> expr \\<times> val \\<times> xstate) set" |
14 evals :: "java_mb prog => (xstate \\<times> expr list \\<times> val list \\<times> xstate) set" |
13 evals :: "java_mb prog => (xstate \\<times> expr list \\<times> val list \\<times> xstate) set" |
15 exec :: "java_mb prog => (xstate \\<times> stmt \\<times> xstate) set" |
14 exec :: "java_mb prog => (xstate \\<times> stmt \\<times> xstate) set" |
16 |
15 |
17 syntax |
16 syntax |
18 eval :: "[java_mb prog,xstate,expr,val,xstate] => bool " |
17 eval :: "[java_mb prog,xstate,expr,val,xstate] => bool " |
19 ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,82,82,82] 81) |
18 ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,60,82,82] 81) |
20 evals:: "[java_mb prog,xstate,expr list, |
19 evals:: "[java_mb prog,xstate,expr list, |
21 val list,xstate] => bool " |
20 val list,xstate] => bool " |
22 ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,51,51,82] 81) |
21 ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,60,51,82] 81) |
23 exec :: "[java_mb prog,xstate,stmt, xstate] => bool " |
22 exec :: "[java_mb prog,xstate,stmt, xstate] => bool " |
24 ("_ \\<turnstile> _ -_-> _" [51,82,82,82] 81) |
23 ("_ \\<turnstile> _ -_-> _" [51,82,60,82] 81) |
25 |
24 |
26 syntax (HTML) |
25 syntax (HTML) |
27 eval :: "[java_mb prog,xstate,expr,val,xstate] => bool " |
26 eval :: "[java_mb prog,xstate,expr,val,xstate] => bool " |
28 ("_ |- _ -_>_-> _" [51,82,82,82,82] 81) |
27 ("_ |- _ -_>_-> _" [51,82,60,82,82] 81) |
29 evals:: "[java_mb prog,xstate,expr list, |
28 evals:: "[java_mb prog,xstate,expr list, |
30 val list,xstate] => bool " |
29 val list,xstate] => bool " |
31 ("_ |- _ -_[>]_-> _" [51,82,51,51,82] 81) |
30 ("_ |- _ -_[>]_-> _" [51,82,60,51,82] 81) |
32 exec :: "[java_mb prog,xstate,stmt, xstate] => bool " |
31 exec :: "[java_mb prog,xstate,stmt, xstate] => bool " |
33 ("_ |- _ -_-> _" [51,82,82,82] 81) |
32 ("_ |- _ -_-> _" [51,82,60,82] 81) |
34 |
33 |
35 |
34 |
36 translations |
35 translations |
37 "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval G" |
36 "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval G" |
38 "G\\<turnstile>s -e \\<succ> v-> s' " == "(s, e, v, s') \\<in> eval G" |
37 "G\\<turnstile>s -e \\<succ> v-> s' " == "(s, e, v, s') \\<in> eval G" |
121 (* cf. 14.7 *) |
120 (* cf. 14.7 *) |
122 Expr "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==> |
121 Expr "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==> |
123 G\\<turnstile>Norm s0 -Expr e-> s1" |
122 G\\<turnstile>Norm s0 -Expr e-> s1" |
124 |
123 |
125 (* cf. 14.2 *) |
124 (* cf. 14.2 *) |
126 Comp "[| G\\<turnstile>Norm s0 -s -> s1; |
125 Comp "[| G\\<turnstile>Norm s0 -s-> s1; |
127 G\\<turnstile> s1 -t -> s2|] ==> |
126 G\\<turnstile> s1 -t -> s2|] ==> |
128 G\\<turnstile>Norm s0 -(s;; t)-> s2" |
127 G\\<turnstile>Norm s0 -s;; t-> s2" |
129 |
128 |
130 (* cf. 14.8.2 *) |
129 (* cf. 14.8.2 *) |
131 Cond "[| G\\<turnstile>Norm s0 -e \\<succ>v-> s1; |
130 Cond "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; |
132 G\\<turnstile> s1 -(if the_Bool v then s else t)-> s2|] ==> |
131 G\\<turnstile> s1 -(if the_Bool v then s else t)-> s2|] ==> |
133 G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2" |
132 G\\<turnstile>Norm s0 -If(e) s Else t-> s2" |
134 |
133 |
135 (* cf. 14.10, 14.10.1 *) |
134 (* cf. 14.10, 14.10.1 *) |
136 Loop "[| G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1 |] ==> |
135 Loop "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; |
137 G\\<turnstile>Norm s0 -(While(e) s)-> s1" |
136 if the_Bool v then G\\<turnstile>s1 -s-> s2 \\<and> G\\<turnstile>s2 -While(e) s-> s3 |
|
137 else s3 = s1 |] ==> |
|
138 G\\<turnstile>Norm s0 -While(e) s-> s3" |
|
139 |
|
140 monos |
|
141 if_def2 |
138 |
142 |
139 end |
143 end |