equal
deleted
inserted
replaced
13 IF b THEN step [s \<leftarrow> S. bval b s] c1 ELSE step [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 S ({Inv} WHILE b DO c {P}) = |
15 "step S ({Inv} WHILE b DO c {P}) = |
16 {S @ post c} WHILE b DO (step [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 |
|
19 text{* Examples: *} |
|
20 |
|
21 definition "c = WHILE Less (V ''x'') (N 3) |
|
22 DO ''x'' ::= Plus (V ''x'') (N 2)" |
19 definition "c0 = anno [] c" |
23 definition "c0 = anno [] c" |
20 |
24 |
21 definition "show_acom xs = map_acom (map (show_state xs))" |
25 definition "show_acom xs = map_acom (map (show_state xs))" |
22 |
26 |
|
27 |
23 text{* Collecting semantics: *} |
28 text{* Collecting semantics: *} |
24 |
29 |
25 value "show_acom [''x''] (((step [<>]) ^^ 6) c0)" |
30 value "show_acom [''x''] (((step [<>]) ^^ 6) c0)" |
|
31 |
26 |
32 |
27 text{* Small step semantics: *} |
33 text{* Small step semantics: *} |
28 |
34 |
29 value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))" |
35 value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))" |
30 |
36 |