2 imports ACom |
2 imports ACom |
3 begin |
3 begin |
4 |
4 |
5 subsection "Executable Collecting Semantics on lists" |
5 subsection "Executable Collecting Semantics on lists" |
6 |
6 |
7 fun step_cs :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where |
7 fun step :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where |
8 "step_cs S (SKIP {P}) = (SKIP {S})" | |
8 "step S (SKIP {P}) = (SKIP {S})" | |
9 "step_cs S (x ::= e {P}) = |
9 "step S (x ::= e {P}) = |
10 (x ::= e {[s(x := aval e s). s \<leftarrow> S]})" | |
10 (x ::= e {[s(x := aval e s). s \<leftarrow> S]})" | |
11 "step_cs S (c1; c2) = step_cs S c1; step_cs (post c1) c2" | |
11 "step S (c1; c2) = step S c1; step (post c1) c2" | |
12 "step_cs S (IF b THEN c1 ELSE c2 {P}) = |
12 "step S (IF b THEN c1 ELSE c2 {P}) = |
13 IF b THEN step_cs [s \<leftarrow> S. bval b s] c1 ELSE step_cs [s\<leftarrow>S. \<not> bval b s] c2 |
13 IF b THEN step [s \<leftarrow> S. bval b s] c1 ELSE step [s\<leftarrow>S. \<not> bval b s] c2 |
14 {post c1 @ post c2}" | |
14 {post c1 @ post c2}" | |
15 "step_cs S ({Inv} WHILE b DO c {P}) = |
15 "step S ({Inv} WHILE b DO c {P}) = |
16 {S @ post c} WHILE b DO (step_cs [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}" |
16 {S @ post c} WHILE b DO (step [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}" |
17 |
17 |
18 definition "c = WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)" |
18 definition "c = WHILE Less (V ''x'') (N 2) DO ''x'' ::= Plus (V ''x'') (N 1)" |
19 definition "c0 = anno [] c" |
19 definition "c0 = anno [] c" |
20 |
20 |
21 definition "show_acom xs = map_acom (map (show_state xs))" |
21 definition "show_acom xs = map_acom (map (show_state xs))" |
22 |
22 |
23 value "show_acom [''x''] (((step_cs [<>]) ^^ 6) c0)" |
23 text{* Collecting semantics: *} |
|
24 |
|
25 value "show_acom [''x''] (((step [<>]) ^^ 6) c0)" |
|
26 |
|
27 text{* Small step semantics: *} |
|
28 |
|
29 value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))" |
24 |
30 |
25 end |
31 end |