equal
deleted
inserted
replaced
29 |
29 |
30 Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
30 Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
31 |
31 |
32 code_pred big_step . |
32 code_pred big_step . |
33 |
33 |
34 (* FIXME: example state syntax *) |
|
35 values "{map t [''x'',''y'',''z''] |t. |
34 values "{map t [''x'',''y'',''z''] |t. |
36 (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}" |
35 (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}" |
37 |
36 |
38 values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}" |
37 values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}" |
39 |
38 |
40 end |
39 end |